Name
Abstract | ||
|---|---|---|
iCMTC is an advanced Communication Based Train Control system developed by CASCO Signal Ltd. For China's 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. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1109/APSEC.2014.62 | APSEC (1) |
Keywords | Field | DocType |
block system specification,zone controller,refinement mechanism,finite automata,formal design,verification complexity reduction,specific block layouts,block system complexity,communication based train control system,automated proof,icmtc,traffic engineering computing,event-b notation,railway systems,control engineering computing,verification,casco signal ltd,rodin plug-in,rail traffic control,computational complexity,theorem proving,railway communication,shanghai metro line 10,double slip connection,event-b,formal specification,chinas mass transit transportation,formal verification,zc behavior verification,layout,switches | Formal design,Control theory,Notation,Computer science,Correctness,Real-time computing,Formal methods,Control system,Mathematical properties,Formal verification | Conference |
Volume | ISSN | Citations |
1 | 1530-1362 | 0 |
PageRank | References | Authors |
0.34 | 11 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jie Qian | 1 | 0 | 1.01 |
| Jing Liu | 2 | 250 | 27.30 |
| Chen Xiang | 3 | 31 | 35.72 |
| Junfeng Sun | 4 | 13 | 9.16 |