CSP Based Modeling And Verification Of CBTC Zone Controller System

the most mainstreaming city track traffic control system, the Communication-Based Crain Control (CBTC) systems owns the self-evident importance of system security. Zone Controller(ZC), as one of the subsystems in CBTC, it plays the role of train management,mobile authorization computing and such functions related with security.In the systems development process,scene of complex systems can lead to logical loopholes of demanding description,which consequentially cause some logical conflicts in the system.This essay extracts the scene specification for modeling and verification according to different scenarios, in order to prove that there is no logical conflicts in the requirements of scene of Zone Controller,for the benefit that the subsystem logical correctness of software requirements can be specificly ensured.In the beginning,the essay bases on the structure and function of the Zone Controller system, and starts from the UML semi-formal description,obtaining the CSP model of CBTC Zone Controller in accordance with the model transformation rules. Furthermore,it switchs the model into CSPM language which can be identified by PROB.Additionally, PROB software is applied to verify the deadlock, livelock and deterministic.,After that,it extracts Zone Controller’s demands standard of eight normal traffic scenes and three failure scenarios descriptions of requirement specification.Finally,it verifies the demands model’s logicality with CSP modeling and verification methods, in order to provethe availability of methods.