Automated Verification of Signalling Principles in Railway Interlocking Systems

DOI10.1016/J.ENTCS.2009.08.015MaRDI QIDQ5178972zbMATH OpenOpenAlexWikidataFDO

Authors Karim Kanso, Anton Setzer, Faron Moller

Publication date 18 March 2015

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.08.015

zbMATH Keywords

automated theorem provingladder logicrailway interlocking systemssafety propertiesSAT solverssignalling principlesverification

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems involving computers (process control, etc.) (93C83)

Recommendations

• Formal verification of a railway interlocking system using model checking
• scientific article; zbMATH DE number 2086584
• Automated validation and verification of railway specific components and systems.
• scientific article; zbMATH DE number 2090138
• A formal approach for the construction and verification of railway control systems

Cites work

• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• Present and Future of Practical SAT Solving

Cited in

(12)

• Case study: Formal verification of a computerized railway interlocking
• Formal verification of a railway interlocking system using model checking
• Stepwise development and model checking of a distributed interlocking system using RAISE
• Stepwise development and model checking of a distributed interlocking system -- using RAISE
• Efficient data validation for geographical interlocking systems
• Security codes in railway interlocking systems.
• MODELING FIXED-BLOCK RAILWAY SIGNALING SYSTEM USING CELLULAR AUTOMATA MODEL
• scientific article; zbMATH DE number 6513409 (Why is no real title available?)
• Automated validation and verification of railway specific components and systems.
• Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans
• scientific article; zbMATH DE number 2090138 (Why is no real title available?)
• A light-weight integration of automated and interactive theorem proving

Describes a project that uses

Uses Software

• OKlibrary

This page was built for publication: Automated Verification of Signalling Principles in Railway Interlocking Systems

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