Title :
Formal Approaches to Mode Conversion and Positioning for Vehicle System
Author :
Su, Wen ; Yang, Fan ; Wu, Xiaofeng ; Guo, Jian ; Zhu, Huibiao
Author_Institution :
Software Eng. Inst., East China Normal Univ., Shanghai, China
Abstract :
The mode conversion and positioning of the vehicle subsystem of the Communication Based Train Control System (CBTC), need to be safe and reliable, being two critical components. To meet this requirement, we apply formal methods in the design of rail transport systems. This paper studies the specification and verification of the mode conversion and positioning system. The mode conversion system is studied by using Communicating Sequential Processes (CSP) combined with simple data structure. The positioning system is explored by combining CSP with Object-Z (OZ). Based on the achieved model, the safety property verification and simulation are proceeded by the automatic process analysis toolkit PAT.
Keywords :
communicating sequential processes; control engineering computing; data structures; formal specification; formal verification; light rail systems; position control; railway safety; CSP; Object-Z; PAT; automatic process analysis toolkit; communicating sequential processes; communication based train control system; data structure; formal approach; mode conversion; positioning system; rail transport systems; safety property verification; specification; vehicle system; Acceleration; Control systems; Data structures; Safety; Synchronization; System recovery; Vehicles; CSP; OZ; PAT; industrial project; software engineering;
Conference_Titel :
Computer Software and Applications Conference Workshops (COMPSACW), 2011 IEEE 35th Annual
Conference_Location :
Munich
Print_ISBN :
978-1-4577-0980-7
Electronic_ISBN :
978-0-7695-4459-5
DOI :
10.1109/COMPSACW.2011.76
