Formal Modeling Of UPPAAL Based ETCS-1/ETCS-NTC Level Transition

Compared with aviation,automobile and other transport modes,rail transport has the advantages of large passenger volumes,eco-friendly,high punctuality rate,which makes rail transport play a key role in the transport system.Train operation control system is an important component of railway signal,it is the key subsystem to ensure the safety of traveling,improve the transportation efficiency and increase speed.With the implementation of China's "One Belt One Road" policy,the issue how to meet the interoperability requirements and ensure safety has become the focus of railway signal industry.European Train Control System is to develop and to deploy a single harmonised control,command,signalling system that is fully interoperable across borders,and its evolution is based on compatibility.The transition between ETCS application Level 1 and Level NTC is a sort of transition between European train control system and national train control system.Therefore,it is necessary to study the transformation between them.Formal modeling is used to design and verify system,which can ensure the correction and security in design and development period.This thesis is on the basis of ETCS System Requirement Specification,Specific Transimission Module FFFIS,and Performance Requirement for Interoperability.We establish a timed automation model of Level 1/Level NTC transition focus on information exchange among ETCS on-board subsystem,trackside subsystem and system environment.The model is verified by both simulation and formal verification in the end.First of all,this thesis introduces ETCS from two aspects:system function structure and application levels,expounds the application scope,the structure of system,system environment and application status of ETCS.Secondly,we analyse three scenes:start of mission in Level 1 and establish connection to specific transmission module,transition from Level 1 to Level NTC,transition from Level NTC to Level 1.Then establish independent timed automata models for the onboard equipments,trackside and the driver.Finally,according to the principle of timed automation,combine all independent time automatic machines into time automation network model,and the network model is simulated and verified in UPPAAL.We use BNF to verify the real-time and safety properties of the whole network,reach the goal of model verification,the result shows that the model can meet the performance requirement of system,provide a reference for the design of train control system.