The authors introduce the concept for a distributed railway control system and present the specification and verification of the main algorithm used for safe distributed control. Our design and verification approach is based on the RAISE method, starting with highly abstract algebraic specifications which are transformed into directly implementable distributed control processes by applying a series of refinement and verification steps. Concrete safety requirements are derived from an abstract version that can be easily validated with respect to soundness and completeness. Complexity is further reduced by separating the system model into a domain model and a controller model. The domain model describes the physical system in absence of control and the controller model introduces the safety-related control mechanisms as a separate entity monitoring observables of the physical system to decide whether it is safe for a train to move or for a point to be switched.


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

    Formal development and verification of a distributed railway control system


    Beteiligte:

    Erscheinungsdatum :

    2000-01-01


    Anmerkungen:

    Haxthausen , A E & Peleska , J 2000 , ' Formal development and verification of a distributed railway control system ' , IEEE Transaction on Software Engineering , vol. 26 , no. 8 , pp. 687-701 . https://doi.org/10.1109/32.879808



    Medientyp :

    Aufsatz (Zeitschrift)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch


    Klassifikation :

    DDC:    629




    Formal Methods for the Specification and Verification of Distributed Railway Control Systems: From Algebraic Specification to Distributed Hybrid Real-Time Systems

    Peleska, J. / Haxthausen, A. E. / Institut fur Automatisierungstechnik et al. | British Library Conference Proceedings | 2000


    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 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