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.展开更多
With the increasing computing demand of train operation control systems,the application of cloud computing technology on safety computer platforms of train control system has become a research hotspot in recent years....With the increasing computing demand of train operation control systems,the application of cloud computing technology on safety computer platforms of train control system has become a research hotspot in recent years.How to improve the safety and availability of private cloud safety computers is the key problem when applying cloud computing to train operation control systems.Because the cloud computing platform is in an open network environment,it can face many security loopholes and malicious network at-tacks.Therefore,it is necessary to change the existing safety computer platform structure to improve the attack resistance of the private cloud safety computer platform,thereby enhancing its safety and reliability.Firstly,a private cloud safety computer platform architecture based on dynamic heterogeneous redundant(DHR)structure is proposed,and a dynamic migration mechanism for heterogeneous executives is designed.Then,a generalized stochastic Petri net(GSPN)model of a private cloud safety computer platform based on DHR is established,and its steady-state probability is solved by using its isomorphism with the continuous-time Markov model(CTMC)to analyse the impact of different system structures and executive migration mechanisms on the system's anti-attack performance.Finally,through experimental verifcation,the system structure proposed in this paper can improve the anti-attack capability of the private cloud safety computer platform,thereby improving its safety and reliability.展开更多
基金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.
基金supported by the National Natural Science Foundation of China(Grant No.U1934219)the National Science Fund for Excellent Young Scholars(Grant No.52022010).
文摘With the increasing computing demand of train operation control systems,the application of cloud computing technology on safety computer platforms of train control system has become a research hotspot in recent years.How to improve the safety and availability of private cloud safety computers is the key problem when applying cloud computing to train operation control systems.Because the cloud computing platform is in an open network environment,it can face many security loopholes and malicious network at-tacks.Therefore,it is necessary to change the existing safety computer platform structure to improve the attack resistance of the private cloud safety computer platform,thereby enhancing its safety and reliability.Firstly,a private cloud safety computer platform architecture based on dynamic heterogeneous redundant(DHR)structure is proposed,and a dynamic migration mechanism for heterogeneous executives is designed.Then,a generalized stochastic Petri net(GSPN)model of a private cloud safety computer platform based on DHR is established,and its steady-state probability is solved by using its isomorphism with the continuous-time Markov model(CTMC)to analyse the impact of different system structures and executive migration mechanisms on the system's anti-attack performance.Finally,through experimental verifcation,the system structure proposed in this paper can improve the anti-attack capability of the private cloud safety computer platform,thereby improving its safety and reliability.