Formal verification of a railway interlocking system using model checking

DOI10.1007/S001650050022MaRDI QIDQ1295868zbMATH OpenOpenAlexDBLPWikidataFDO

Authors V. Pereyra, Alessandro Cimatti, Fausto Giunchiglia, Giovanni Mongardi, Daniela Romano, F. Torielli, Paolo Traverso

Publication date 26 July 1999

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s001650050022

zbMATH Keywords

industrial application of formal methods

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Computing methodologies and applications (68U99)

Recommendations

• Case study: Formal verification of a computerized railway interlocking
• Automated Verification of Signalling Principles in Railway Interlocking Systems
• A formal approach for the construction and verification of railway control systems
• Model checking at IBM
• Stepwise development and model checking of a distributed interlocking system -- using RAISE

Cited in

(12)

• Case study: Formal verification of a computerized railway interlocking
• A system-based approach to the formal development of embedded controllers for a railway
• Stepwise development and model checking of a distributed interlocking system using RAISE
• Stepwise development and model checking of a distributed interlocking system -- using RAISE
• Formal verification of safety protocol in train control system
• scientific article; zbMATH DE number 1629970 (Why is no real title available?)
• A logic approach to decision taking in a railway interlocking system using Maple
• scientific article; zbMATH DE number 2090138 (Why is no real title available?)
• Automated Verification of Signalling Principles in Railway Interlocking Systems
• A formal approach for the construction and verification of railway control systems
• A logic-algebraic approach to decision taking in a railway interlocking system
• Verification of configurable SRA systems

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: Formal verification of a railway interlocking system using model checking

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