Formal verification of safety protocol in train control system

Zhang, Yan; Tang, Tao; Li, KePing; Mera Sánchez De Pedro, José Manuel; Zhu, Li; Zhao, Lin y 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.

Descripción

Título: Formal verification of safety protocol in train control system
Autor/es:
  • Zhang, Yan
  • Tang, Tao
  • Li, KePing
  • Mera Sánchez De Pedro, José Manuel
  • Zhu, Li
  • Zhao, Lin
  • Xu, TianHua
Tipo de Documento: Artículo
Título de Revista/Publicación: SCIENCE CHINA Technological Sciences
Fecha: 2011
Volumen: 11
Materias:
Palabras Clave Informales: train control system – safety communication protocol – interface automata – verification
Escuela: E.T.S.I. Industriales (UPM)
Departamento: Ingeniería Mecánica y de Fabricación [hasta 2014]
Licencias Creative Commons: Reconocimiento - Sin obra derivada - No comercial

Texto completo

[img]
Vista Previa
PDF (Document Portable Format) - Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (1MB) | Vista Previa

Resumen

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.

Más información

ID de Registro: 12332
Identificador DC: http://oa.upm.es/12332/
Identificador OAI: oai:oa.upm.es:12332
Identificador DOI: 10.1007/s11431-011-4562-2
URL Oficial: http://www.springerlink.com/content/xv40047201w57873/
Depositado por: Memoria Investigacion
Depositado el: 27 Ago 2012 12:21
Ultima Modificación: 21 Abr 2016 11:34
  • Open Access
  • Open Access
  • Sherpa-Romeo
    Compruebe si la revista anglosajona en la que ha publicado un artículo permite también su publicación en abierto.
  • Dulcinea
    Compruebe si la revista española en la que ha publicado un artículo permite también su publicación en abierto.
  • Recolecta
  • e-ciencia
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM