A formal approach for the construction and verification of railway control systems

DOI10.1007/S00165-009-0143-6MaRDI QIDQ539161zbMATH OpenOpenAlexFDO

Authors Jan Peleska, Sebastian Kinder, Anne Elisabeth Haxthausen

Publication date 27 May 2011

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

Full work available at URL https://doi.org/10.1007/s00165-009-0143-6

zbMATH Keywords

verificationformal methodsdomain-specific languagescode generationdomain engineeringrailway control systems

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Application models in control theory (93C95)

Recommendations

• A Domain-Oriented, Model-Based Approach for Construction and Verification of Railway Control Systems
• A system-based approach to the formal development of embedded controllers for a railway
• Automated validation and verification of railway specific components and systems.
• Formal verification of a railway interlocking system using model checking
• Stepwise development and model checking of a distributed interlocking system -- using RAISE

Cites work

• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• Domain engineering
• The code validation tool (CVT). Automatic verification of a compilation process

Cited in

(24)

• Formal verification of safety protocol in train control system
• A system-based approach to the formal development of embedded controllers for a railway
• Automated validation and verification of railway specific components and systems.
• Stepwise development and model checking of a distributed interlocking system using RAISE
• Automatic verification of safety rules for a subway control software
• Stepwise development and model checking of a distributed interlocking system -- using RAISE
• A refinement-based approach to deriving train controllers
• Using SCR to specify requirements of the BART advanced automated train control system
• Verification of a controller for BART: An approach based on Horn logic and denotational semantics
• Automating Verification of Cooperation, Control, and Design in Traffic Applications
• A logic-algebraic approach to decision taking in a railway interlocking system
• An approach from answer set programming to decision making in a railway interlocking system
• Modeling and verification of control system specification for railway level crossings based on formal method
• A Domain-Oriented, Model-Based Approach for Construction and Verification of Railway Control Systems
• Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application
• A case in point: verification and testing of a EULYNX interface
• Formal Approach to Railway Applications
• Automated Verification of Signalling Principles in Railway Interlocking Systems
• scientific article; zbMATH DE number 2086584 (Why is no real title available?)
• Verification of a radio-based signaling system using the STATEMATE verification environment
• Supporting design and developement of safety critical applications by model based tools
• Dynamic state machines for formalizing railway control system specifications
• Specification and validation of a concurrent system: An educational project
• Manifest domains: analysis and description

Describes a project that uses

Uses Software

• CVT
• SystemC

This page was built for publication: A formal approach for the construction and verification of railway control systems

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