期刊文献+

Formal verification of safety protocol in train control system 被引量:6

Formal verification of safety protocol in train control system
原文传递
导出
摘要 In order to satisfy the safety-critical requirements,the train control system(TCS) often employs a layered safety communication protocol to provide reliable services.However,both description and verification of the safety protocols may be formidable due to the system complexity.In this paper,interface automata(IA) are used to describe the safety service interface behaviors of safety communication protocol.A formal verification method is proposed to describe the safety communication protocols using IA and translate IA model into PROMELA model so that the protocols can be verified by the model checker SPIN.A case study of using this method to describe and verify a safety communication protocol is included.The verification results illustrate that the proposed method is effective to describe the safety protocols and verify deadlocks,livelocks and several mandatory consistency properties.A prototype of safety protocols is also developed based on the presented formally verifying method.
出处 《Science China(Technological Sciences)》 SCIE EI CAS 2011年第11期3078-3090,共13页 中国科学(技术科学英文版)
基金 supported by the New Century Excellent Researcher Award Program from Ministry of Education of China (Grant No. NCET-07-0059) the Fundamental Research Funds for the Central Universities (Grant No.2011YJS006) the National High Technology Research and DevelopmentProgram of China ("863" Program) (Grant No. 2011AA010104) the State Key Laboratory of Rail Traffic Control and Safety Research Project(Grant Nos. RCS2008ZZ001, RCS2008ZZ005)
关键词 train control system safety communication protocol interface automata VERIFICATION 列车控制系统 形式化验证 安全协议 安全通信协议 接口自动机 安全服务 核查方法 模型检查
  • 相关文献

参考文献34

二级参考文献78

共引文献73

同被引文献40

引证文献6

二级引证文献14

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部