Stepwise development and model checking of a distributed interlocking system using RAISE

DOI10.1007/S00165-020-00507-2MaRDI QIDQ1996429zbMATH OpenOpenAlexWikidataFDO

Authors S. Geisler, Anne Elisabeth Haxthausen

Publication date 4 March 2021

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

Full work available at URL https://orbit.dtu.dk/en/publications/a41f95b0-cecb-4480-819e-ddaaea81554d

zbMATH Keywords

model checkingdistributed systemsrailway interlocking systemsRAISEstepwise development

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Traffic problems in operations research (90B20) Networked control (93B70)

Recommendations

• Stepwise development and model checking of a distributed interlocking system -- using RAISE
• Formal verification of a railway interlocking system using model checking
• scientific article; zbMATH DE number 1324647
• A formal approach for the construction and verification of railway control systems
• Automated Verification of Signalling Principles in Railway Interlocking Systems

Cites work

• scientific article; zbMATH DE number 795688 (Why is no real title available?)
• A state/event-based model-checking approach for the analysis of abstract system properties
• Abstract state machines, Alloy, B, TLA, VDM, and Z. 6th international conference, ABZ 2018, Southampton, UK, June 5--8, 2018. Proceedings
• Model checking RAISE applicative specifications
• Stepwise development and model checking of a distributed interlocking system -- using RAISE

Cited in

(4)

• Stepwise development and model checking of a distributed interlocking system -- using RAISE
• A Domain-Oriented, Model-Based Approach for Construction and Verification of Railway Control Systems
• Efficient data validation for geographical interlocking systems
• scientific article; zbMATH DE number 2090138 (Why is no real title available?)

Describes a project that uses

Uses Software

• SAL
• RAISE

This page was built for publication: Stepwise development and model checking of a distributed interlocking system using RAISE

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