维普中文期刊产品整合服务

Formal verification of safety protocol in train control system

查看全文 作  者:ZHANG [1]Yan;TANG [1]Tao;LI [1]KePing;MERA Jose [2]Manuel;ZHU [1]Li;ZHAO [1]Lin;XU [1]TianHua 高影响力作者 机构地区:[1]State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, Beijing 100044, China;[2]Railway Technologies Research Centre, Universidad Politecnica de Madrid, Madrid 228006, Spain高影响力机构 出  处:《Science China(Technological Sciences)》索引2011年第54卷第11期,共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) 摘  要: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. 关 键 词:列车控制系统 形式化验证 安全协议 安全通信协议 接口自动机 安全服务 核查方法 模型检查
相关文献

参考文献(34)

引证文献(6)

耦合文献(82)

网站首页 | 关于我们 | 联系我们 | 产品服务 | 客服中心 | 广告服务 | 版权声明 | 网站联盟 | 友情链接 | 售卡网点

版权所有© 渝B2-20050021-1 渝公网安备 50019002500403号 违法和不良信息举报中心

互联网出版许可证 新出网证(渝)字10号 全国400电话 - 免长途话费