Safety Monitoring of Communication Session for CTCS-3
The safety of the communication session for CTCS-3 is of high importance. The method, using the framework of properties monitoring, is given to make sure the communication session running safely. In this framework, the relevant properties are described by finite LTL formulae. Then the framework is applied in the communication initiation process. Through analyzing the finite trace of the running system, the method is proved to be able to detect violations of safety properties. The method turns out to be feasible and appropriate for the verification of train control system.
properties monitoring rewriting logic communication session Maude
Ming Chai Xian Li Lin Zhao Tao Tang
State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, Beijing
国际会议
2010 Cross-Strait Conference on Information Science and Technology(2010 海峡两岸信息科学与技术学术交流会)
秦皇岛
英文
529-532
2010-07-09（万方平台首次上网日期，不代表论文的发表时间）