TY - GEN
T1 - Formal design and verification of zone controller
AU - Qian, Jie
AU - Liu, Jing
AU - Chen, Xiang
AU - Sun, Junfeng
N1 - Publisher Copyright:
© 2014 IEEE.
PY - 2014
Y1 - 2014
N2 - iCMTC is an advanced Communication Based Train Control system developed by CASCO Signal Ltd. for Chinas mass transit transportation. Some subsystems of iCMTC has been applied in Shanghai Metro Line 10. Zone Controller (ZC) is one of the subsystems of iCMTC. Modeling and verifying ZC is challenging due to the complexity of the block system and the behavior itself. We propose a formal approach to gradually specify the block system and lower complexity of the verification of ZC behavior. In recent years, there are many researches on railway systems. However, these studies use simple track networks, which makes them inadequate in industrial practice. To address this problem, we define specific block layouts (i.e., double slip connection) as relations on sets. We also define mathematical properties of the relations so that the block system can be precisely described. For the purpose of reducing the complexity of verification, we propose an improved refinement mechanism based on the Event-B notation. Based on this refinement mechanism, we develop a Rodin plug-in to help us refine the system. We use this mechanism in modeling the ZC behavior, and achieve good results in automated proof. Several safety properties are considered and verified to ensure the safety and correctness of ZC.
AB - iCMTC is an advanced Communication Based Train Control system developed by CASCO Signal Ltd. for Chinas mass transit transportation. Some subsystems of iCMTC has been applied in Shanghai Metro Line 10. Zone Controller (ZC) is one of the subsystems of iCMTC. Modeling and verifying ZC is challenging due to the complexity of the block system and the behavior itself. We propose a formal approach to gradually specify the block system and lower complexity of the verification of ZC behavior. In recent years, there are many researches on railway systems. However, these studies use simple track networks, which makes them inadequate in industrial practice. To address this problem, we define specific block layouts (i.e., double slip connection) as relations on sets. We also define mathematical properties of the relations so that the block system can be precisely described. For the purpose of reducing the complexity of verification, we propose an improved refinement mechanism based on the Event-B notation. Based on this refinement mechanism, we develop a Rodin plug-in to help us refine the system. We use this mechanism in modeling the ZC behavior, and achieve good results in automated proof. Several safety properties are considered and verified to ensure the safety and correctness of ZC.
KW - Event-B
KW - Formal design
KW - Verification
KW - Zone controller
UR - https://www.scopus.com/pages/publications/84951290151
U2 - 10.1109/APSEC.2014.62
DO - 10.1109/APSEC.2014.62
M3 - 会议稿件
AN - SCOPUS:84951290151
T3 - Proceedings - Asia-Pacific Software Engineering Conference, APSEC
SP - 375
EP - 382
BT - Proceedings - 21st Asia-Pacific Software Engineering Conference, APSEC 2014
A2 - Gueheneuc, Yann-Gael
A2 - Kwon, Gihwon
A2 - Cha, Sungdeok
PB - IEEE Computer Society
T2 - 21st Asia-Pacific Software Engineering Conference, APSEC 2014
Y2 - 1 December 2014 through 4 December 2014
ER -