Modeling And Verification Of ZC Subsystem Based On Timed Automata

As urbanization process has accelerated and urban rail transit has developed rapidly in recent years,Communication Based Train Control(CBTC)system has been increasingly and widely used.Zone Controller(ZC)as the ground kernel subsystem of CBTC system,calculates Movement Authority(MA)information for trains in real time through the interactive communications with other equipments,realizing interval controls on trains.ZC subsystem serves as a typical real-time system,which correct logicality and time sequence have great significance to the safety of the system in the migration process of behavior state.In this connection,in order to further ensure that ZC subsystem can operate safely to achieve its functions,a method based on timed automata is proposed for modeling and verifying ZC subsystem.By modeling the system,this thesis verified and analyzed whether safety requirements can be met when the system operates in terms of logicality and time sequence.Firstly,this thesis analyzes the features of ZC subsystem and adopts gradational structure ideas to divide ZC subsystem into system equipment layer and function logic layer.Secondly,based on the extended modes of UML and the characteristics of ZC subsystem,this thesis extends sequential graphical element model reasonably in the two aspects of clock constraint and variables,making it fully describe the logicality and time sequence of system in the interaction process.Then,according to model transformation theory and on the basis of ensuring the consistency of model transformation process,this thesis transforms semi-formal extended sequence diagram into formal timed automata model with reasonable transformational rules.This thesis also summarizes the classification of formal verification methods,and expounds the basic structure and functions of the verification tool UPPAAL of timed automata model.On this basis,this thesis analyzes the logical semantics conversion from LTL formula to BNF formula.Finally,this thesis selects the two scenes of MA retracement and train acrossing the border from ZC zone to make analyses,setting up timed automata model respectively,and a timed automata network model is established in UPPAAL software.Through verifying the logicality and time sequence of system requirements in the two different scenes,the safe operation of the system is ensured in terms of logicality and time sequence.That is how prove the feasibility and effectiveness of the modeling and verification methods which are proposed in this paper.