Modeling,Verification And Application Of Compilation Rules Of Balise Telegram

Balise system is an important equipment to achieve the wayside-onboard information transmission.The correctness of the balise telegram is directly related to train operation safety.The balise telegram is compiled from the line engineering data by the compiler according to the balise application principle.However,the application principle only defines the setting principle of balise and the telegram structure from the perspective of the functional requirements of the train control system,and does not specifically describe how to compile telegram.In addition,The balise application principle based on text language is easy to produce ambiguous problem.There are great hidden dangers in translating the application principle into the related software code.In order to solve the above problems,a modeling and verification method framework for balise telegram rules is proposed.It establishes a bidirectional track chain for balise compilation rules,models,verification process and verification results.By analyzing the model checking results,we can continuously modify the rule models,so as to get correct and unambiguous balise telegram rule models,which can be used to guide the telegram compilation and related tools.This is important to ensure the correctness of the balise telegram and to support the revision of the technical specifications.Based on the above framework,the following work has been done:(1)From the perspective of data life cycle and data structure,the balise telegram is analyzed,and the whole process of telegram data generation,usage,and storage is summarized.The structural model of engineering data and telegram data is established.Then,the content of the balise application principles and the related expert experiences are digged deeply,which is the basis for the modeling and verification of telegram compilation rules.(2)Taking the relevant specification and expert experience of balise telegram compilation as input,the overall frame of telegram compilation rules is extracted.Besides,taking the telegram generation scenario corresponding to a particular type of balise as an example,the compilation rules are modeled and verified.First of all,we analyzed the rules non-formally to output the rules management reports,which can achieve the forward tracking of the rules to the models.Then,we established formal models of the rules by using method which is the combination of UML and NuSMV,and inputed the models into the verification tool.After that,we constantly modified the errors in the counter examples until the results are all true.Finally,the rules and corresponding models are obtained which could meet the quality requirements.(3)Based on the rules and the models,an automation tool used for telegram compilation was developed.Taking the actual line data as an example to compile the balise telegram,and comparing the telegram which generated by the tool with actual route telegram,the results can prove the correctness of the tool.In addition,it can also show that the tool had improved the automation of telegram compilation.The result indicated the correctness and completeness of the rule models,which is help to ensure the correctness of the telegram data and is of great significance for the safe operation of the train control system.