Hybrid Modelling And Verification Of CTCS-3System Specification

System specification is the starting point and foundation of the system development. The defects of the system specification will bring great risks to system development. Modelling and verifying the system specification is an effective method to eliminate potential defects, and it is also a premise to ensure the system be designed and developmented correctly.In recent years, China's railway business has made rapid development. Train control system based on wireless communication, such as CTCS-3, is the future trend of development. CTCS-3system is a typical hybrid system whose entities such as velocity, acceleration, and distance evolve continuously under the guidance of computer which can control the power and brakes and affect the continuous-time dynamics. Train accidents are usually closely related with the bad control of Continuous variables such as velocity, acceleration, distance. Therefore, modelling and verifying the system specification of safty-critical CTCS-3is very necessary and meaningful from the point of view of hybridity.Aimed at this, this paper gives a method and process of hybridity-oriented modelling and verification of CTCS-3system specification based on the modeling and verification architecture of train control system:Firstly, we model the CTC-3system specification using HybridUML which can describe the hybridity of system; then we transfer the HybridUML model of CTCS-3system specification to formal Differential Dynamic Logic model; next, we verify the Differential Dynamic Logic model in verification tool.This paper mainly discusses the process of extending UML2.0to HybridUML in modeling tool RSA by creating profiles. At the same time, taking the acceleration and deceleration process of train as example, this paper expounds the way how to model the CTCS-3system specification using HybridUML. Then, the paper gives the transfer rules from HybridUML model to Differential Dynamic Logic model. Based on these rules, the formal model of CTCS-3system specification can be acquired and the formal verification of the model can be carried out.In the last place, taking RBC handover which is a classical hybrid scenario of CTCS-3as case, this paper gives the application of the hybridity-oriented modeling and verification method of CTCS-3system specification. Firstly, we introduce the process of RBC handover of CTCS-3systen specification; then we model the RBC handover in RSA using HybridUML; nextly,we aquire the Differantial Dynamic Logic model of RBC handover based on the transfer rules; finally, we verify the safety of Differential Dynamic Logic model of RBC handover in KeYmaera and analyse the verification result. The case study correctly shows the method and process of hybrid-oriented modeling and verification, and adequately manifestes the effectiveness and feasibility of the method and process.