In this paper we present an approach for automated verification of train or from control systems which is based on model checking. The strategies and techniques applied are distinguished from comparable concepts of other authors in the following ways: (1) The control model to be verified is equivalent to executable machine code. As a con- sequence, there is no need for stepwise refinement and associated formal verification, in order to establish the conformance between the model and the executable software. (2) The well-known state explosion problems occurring frequently when checking complete railway control models are overcome by a combination of bounded model checking and inductive or compositional reasoning. (3) Since the verification approach is fully automated, it can be applied to each concrete control system, instantiated from a generic system using configuration data encoding the railway network and the routes to be controlled. This offers an alternative to more conventional (semi-formal) verification strategies, where the generic system is fully verified (so-called type certification), but only partial verification is exercised on the concrete instances.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Automated verification for train control systems


    Additional title:

    Automatische Verifikation von Steuerungs- und Regelungssystemen für Züge


    Contributors:


    Publication date :

    2004


    Size :

    14 Seiten, 2 Bilder, 4 Tabellen, 18 Quellen



    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English




    TRAIN VERIFICATION SYSTEM, TRAIN VERIFICATION METHOD AND GROUND DEVICE

    MORIMOTO KAZUNARI | European Patent Office | 2017

    Free access

    TRAIN TRAFFIC AUTOMATED CONTROL SYSTEM

    LESUN ANATOLIJ FEDOROVICH / RJABKOV ALEKSANDR NIKOLAEVICH / EFREMOV SERGEJ VLADIMIROVICH et al. | European Patent Office | 2016

    Free access

    Logic verification of Collision Avoidance System in train control systems

    Xu, Tianhua / Tang, Tao / Gao, Chunhai et al. | IEEE | 2009


    Logic Verification of Collision Avoidance System in Train Control Systems

    Xu, T. / Tang, T. / Gao, C. et al. | British Library Conference Proceedings | 2009


    Reliability verification of train control algorithm for Korean high-speed train

    Jeon, J.-W. / Lee, J.-H. / Lee, J.-D. et al. | British Library Conference Proceedings | 2000