This paper presents a formal model-based methodology to support railway engineers in the design of safe electronic urban railway control systems. The purpose of our research is to overcome the deficiencies of existing traditional design methodologies, namely the incompleteness and the potential presence of contradictions in the system specification resulting from non-formal development techniques. We illustrate the application of the methodology via a case study of a tram-road level crossing protection system. It was chosen partly because it has a simple architecture and a small number of elements, thus it fits the scope limitations of this article. At the same time, it is suitable for presenting all essential features of our methodology. The proposed solution provides a specification/verification environment that facilitates the construction of correct, complete, consistent, and verifiable functional specifications during the development, while hiding all the formal method-related details from the railway engineers writing the specifications. Using this formal model-based methodology, a high-quality functional specification can be achieved, which is guaranteed to be more exhaustive and will contain fewer errors than traditional development.
Formal Modeling and Verification of the Functionality of Electronic Urban Railway Control Systems Through a Case Study
Urban Rail Transit
Urban Rail Transit ; 8 , 3-4 ; 217-245
01.12.2022
29 pages
Aufsatz (Zeitschrift)
Elektronische Ressource
Englisch
Validation of Railway Interlocking Systems by Formal Verification, A Case Study
British Library Conference Proceedings | 2014
|Formal Specification of Railway Control Systems
Springer Verlag | 2013
|Formal verification of protocol specified in LTS for railway signalling systems
British Library Conference Proceedings | 2004
|Enhancing Spacecraft Safety Through Formal Verification of Attitude Control Systems
Springer Verlag | 2025
|