The Construction And Application Of Data Verification Model Of Train Control System Based On Timed Automata

The Communication Based Train Control System(CBTC)is a typical data-driven safety demanding System.Its sub-systems and the integration of each unit to realize the function of the System depend on configuration data,so the security of CBTC System is inseparable from the quality of System data.How to ensure the quality of data,the formal method can express the composition and characteristics of the system accurately and in detail through mathematical description,and the system characteristics can be modeled and verified by formal modeling method;The data verification system based on data constraint rules can accurately locate the specific error of a certain data.In this paper,the method of combining modeling verification and system operation verification is adopted to verify,analyze and check the data of CBTC system,so as to modify errors conveniently and improve data quality.First,the paper analyzes the components of the CBTC system and the data characteristics of the system.Based on this,the data verification method is investigated.Finally,the model verification based on time automata and the verification of the verification system based on data constraint rules are selected.The method can not only describe the constraint relationship between data in mathematical language,but also accurately locate the wrong data through the system operation results.Secondly,under the understanding of the characteristics of CBTC system,the design of data verification scheme and related theoretical knowledge and technology,design the data of CBTC system and analyze the data from the perspective of data development process and data description.According to the characteristics of the analyzed data,the data relationship is divided into three categories: range relationship,association relationship and network topology relationship,and the data constraint rules are summarized according to the classification criteria.Then,based on the summarized data constraint rules,the model design of data verification is carried out.According to the rules,the data entity and its attribute time automaton model describe the data relationship through the state transition.Based on the summarized data constraint rules,the line data of the Daxing Airport Line was modeled and verified from three types of data relationships.Finally,according to the data constraint rules set established in the previous design,the rules are code developed.The data constraint sets are converted into a data rule script library,and the data verification system calls the rule script to verify the input line data.The correctness of the data is tested from the aspects of modeling verification and system verification.The results show that the scheme can effectively and accurately find the defects of the data.