Formal Modeling And Verification For The Rail Transit Control System Designed By SCADE Base On PVS

With the rapid development of the computer microprocessor technology, the design of embedded systems become more complex, especially for the high security system, such as aircraft, rockets, rail transit control systems, etc. Any subtle mistake may result in disastrous consequences and cause huge economic losses. Therefore, how to design and verify a high-reliable system is very important and necessary.Rail transit control system requires high levels of reliability, traditional validation methods alone cannot meet requirements, new modeling and validation method are needed to accomplish the design and implementation. This paper presents a formalized modeling and verification method based on PVS which is suitable for the rail transit control system designed by SCADE Suite. Research on graphical modeling method in SCADE Suite is also involved together with Lustre language translated from the graphical models for the basic Lustre language, including constants, variable, condition, special operators, conversion rules from lustre into PVS are given. While for the extensive Lustre language, the strategy of the transformation are presented. Furthermore, based on the SCADE Suite modeling, the Lustre codes generated from modeling are read and then transformed into PVS theory according to the conversion rules between SCADE and PVS. Through the Ruby script language, a conversion tool called SCADE2PVS which can transfer from Lustre into PVS, is designed and implemented.At last, the feasibility of the presented method is illustrated by the example of train track's switch in the rail transit control system, by the tool SCADE2PVS. The method of transforming models in SCADE Suite into PVS theory is Certain properties in the train track's switch is proved in PVS.