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.


    Access

    Download


    Export, share and cite



    Title :

    Formal Modeling and Verification of the Functionality of Electronic Urban Railway Control Systems Through a Case Study


    Additional title:

    Urban Rail Transit


    Contributors:

    Published in:

    Urban Rail Transit ; 8 , 3-4 ; 217-245


    Publication date :

    2022-12-01


    Size :

    29 pages




    Type of media :

    Article (Journal)


    Type of material :

    Electronic Resource


    Language :

    English





    Validation of Railway Interlocking Systems by Formal Verification, A Case Study

    Bonacchi, A. / Fantechi, A. / Bacherini, S. et al. | British Library Conference Proceedings | 2014


    Formal Development and Verification of Railway Control Systems

    Vu Hong, Linh / Haxthausen, Anne Elisabeth / Peleska, Jan | BASE | 2013

    Free access

    Formal Specification of Railway Control Systems

    Xu, Bingqing / Zhang, Lichen | Springer Verlag | 2013


    Formal verification of protocol specified in LTS for railway signalling systems

    Lee, J.-H. / Hwang, J.-G. / Yoon, Y.-G. et al. | British Library Conference Proceedings | 2004


    Enhancing Spacecraft Safety Through Formal Verification of Attitude Control Systems

    Song, Chi / Peng, Zhuoyue / Hu, Yang et al. | Springer Verlag | 2025