In this article we are discussing Formal Methods for the integrated development and verification of distributed railway control systems, as, for example, applicable in the German FFB approach for radio-based train control, train protection and interlocking. As description techniques both untimed algebraic specifications and hybrid real-time languages are used. Verification is based on refinement proofs. We advocate an approach starting with untimed algebraic specification defining an abstract centralised controller model. Distribution of control components and hybrid real-time properties are gradually introduced on lower refinement levels. A complete specification, refinemt and verification suite has been performed by the authors for a class of so-called simple networks, based on a control concept originally designed by INSY GmbH. To increase the re-usability of design and verification, frameworks and generic theories specialised on the application domain 'railway control systems' are used.
Formal methods for the specification and verification of distributed railway control systems: from algebraic specifications to distributed hybrid real-time systems
2000
9 Seiten, 2 Bilder, 6 Quellen
Conference paper
English
British Library Conference Proceedings | 2000
|Formal Specification of Railway Control Systems
Springer Verlag | 2013
|Formal specifications of railway signalling systems using Stateflow
Tema Archive | 2007
|Towards Domain-Specific Formal Specification Languages for Railway Control Systems
British Library Conference Proceedings | 2001
|