Formal verification of safety protocol in train control system

Zhang, Yan and Tang, Tao and Li, KePing and Mera Sánchez De Pedro, José Manuel and Zhu, Li and Zhao, Lin and Xu, TianHua (2011). Formal verification of safety protocol in train control system. "SCIENCE CHINA Technological Sciences", v. 11 (n. 54); pp. 3078-3090. ISSN 1674-7321. https://doi.org/10.1007/s11431-011-4562-2.

Description

Title: Formal verification of safety protocol in train control system
Author/s:
  • Zhang, Yan
  • Tang, Tao
  • Li, KePing
  • Mera Sánchez De Pedro, José Manuel
  • Zhu, Li
  • Zhao, Lin
  • Xu, TianHua
Item Type: Article
Título de Revista/Publicación: SCIENCE CHINA Technological Sciences
Date: 2011
ISSN: 1674-7321
Volume: 11
Subjects:
Freetext Keywords: train control system – safety communication protocol – interface automata – verification
Faculty: E.T.S.I. Industriales (UPM)
Department: Ingeniería Mecánica y de Fabricación [hasta 2014]
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview

Abstract

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.

More information

Item ID: 12332
DC Identifier: http://oa.upm.es/12332/
OAI Identifier: oai:oa.upm.es:12332
DOI: 10.1007/s11431-011-4562-2
Official URL: http://www.springerlink.com/content/xv40047201w57873/
Deposited by: Memoria Investigacion
Deposited on: 27 Aug 2012 12:21
Last Modified: 21 Apr 2016 11:34
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM