Formal Modeling and Verification of CTCS-N Level Conversion Scenarios
The onboard equipment of Chinese train control system-new(CTCS-N)undertakes more functions of ground equipment.Its function test of CTCS-N is based on field test,which is time-consuming and laborious.Con-structing a model to meet the functional and performance requirements of the system could ensure the safe and effi-cient operation of the train on the line,so a formal modeling and verification method based on timed automata is pro-posed for CTCS-N.Firstly,the level conversion scenarios is selected as the main modeling scenario,extracting the functional and performance requirements in the specification,and combing the information interaction diagram,the time automata models of onboard equipment,balise,temporary speed restriction server and radio block center are built based on UPPAAL.Finally,based on Backus Naur form(BNF)statements,whether the conversion of onboard equipment in normal mode and fault mode have met the requirements is verified.The validation results show that the model meets the requirements of level conversion scenarios.The system functions in this scenario conform to the cor-responding technical specifications,which proves the feasibility of the formal modeling,and provide reference for modeling and validation of CTCS-N system testing,and other scenarios or functionalities.
Chinese train control system-new(CTCS-N)timed automatalevel conversion scenariomodeling and verificationmessage sequence diagram
万方数据
维普
