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, i...

Full description

Saved in:
Bibliographic Details
Published in:Science China Technological Sciences 2011-11, Vol.54 (11), p.3078-3090
Main Authors: Zhang, Yan, Tang, Tao, Li, KePing, Mera, Jose Manuel, Zhu, Li, Zhao, Lin, Xu, TianHua
Format: Article
Language:English
Subjects:
Checkers
China
Communication systems
Consistency
Control systems
Engineering
Mathematical models
Safety
Trains
列车控制系统
安全协议
安全服务
安全通信协议
形式化验证
接口自动机
核查方法
模型检查
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1674-7321
1869-1900
1862-281X
DOI:10.1007/s11431-011-4562-2