To ensure the correctness of train control system design and development,the ways of simulation,test and formalization were compared.According to the safe critical attribute of train control system,the characters rela...To ensure the correctness of train control system design and development,the ways of simulation,test and formalization were compared.According to the safe critical attribute of train control system,the characters related to system safety were propounded such as real time,hybrid,distribution(concurrence)and reactivity,and the specific formal methods associated with every character were introduced in details.The analysis and classification of the methods were done based on their mathematical basis and applications,and their advantages and disadvantages were given.Analysis result indicates that every method has determinate limitations,which is determined by the essences of model checking and theory proving.It is pointed out that the presentation of new method,the expansion of existing methods and the integration of many methods will be the development trend of formalization in train control system.展开更多
基金This work is supported by Research projects of Beijing National Railway Research and Design Institute of Signal and Communication Co Ltd(No.2300-K1220007)。
文摘To ensure the correctness of train control system design and development,the ways of simulation,test and formalization were compared.According to the safe critical attribute of train control system,the characters related to system safety were propounded such as real time,hybrid,distribution(concurrence)and reactivity,and the specific formal methods associated with every character were introduced in details.The analysis and classification of the methods were done based on their mathematical basis and applications,and their advantages and disadvantages were given.Analysis result indicates that every method has determinate limitations,which is determined by the essences of model checking and theory proving.It is pointed out that the presentation of new method,the expansion of existing methods and the integration of many methods will be the development trend of formalization in train control system.
