Formal verification of safety protocol in train control system

DOI10.1007/S11431-011-4562-2MaRDI QIDQ2321189zbMATH OpenOpenAlexFDO

Authors Yan Zhang, Tao Tang, Ke-Ping Li, Jose Manuel Mera, Lin Zhao, L. Zhu, Tianhua Xu

Publication date 28 August 2019

Published in Science China. Technological Sciences (Search for Journal in Brave)

Full work available at URL http://oa.upm.es/12332/

zbMATH Keywords

verificationinterface automatasafety communication protocoltrain control system

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems involving computers (process control, etc.) (93C83)

Recommendations

• A formal approach for the construction and verification of railway control systems
• Formal verification of a railway interlocking system using model checking
• Verifying RTECTL properties of a train controller systems
• Automatic verification of safety rules for a subway control software

Cites work

• scientific article; zbMATH DE number 1956488 (Why is no real title available?)
• scientific article; zbMATH DE number 2080757 (Why is no real title available?)
• scientific article; zbMATH DE number 1903369 (Why is no real title available?)
• scientific article; zbMATH DE number 2112452 (Why is no real title available?)
• Dependability analysis of the data communication system in train control system
• Extending UML sequence diagrams to model trust-dependent behavior with the aim to support risk analysis
• Synchronous and Bidirectional Component Interfaces

Cited in

(4)

• Automatic verification of safety rules for a subway control software
• Modeling and verification of control system specification for railway level crossings based on formal method
• Formal modeling and verification for MVB
• Verifying a scheduling protocol of safety-critical systems

Describes a project that uses

Uses Software

• vUML
• SPIN

This page was built for publication: Formal verification of safety protocol in train control system

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2321189)