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.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Automated verification for train control systems


    Weitere Titelangaben:

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


    Beteiligte:
    Peleska, Jan (Autor:in) / Große, Daniel (Autor:in) / Haxthausen, Anne E. (Autor:in) / Drechsler, Rolf (Autor:in)


    Erscheinungsdatum :

    2004


    Format / Umfang :

    14 Seiten, 2 Bilder, 4 Tabellen, 18 Quellen



    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    TRAIN VERIFICATION SYSTEM, TRAIN VERIFICATION METHOD AND GROUND DEVICE

    MORIMOTO KAZUNARI | Europäisches Patentamt | 2017

    Freier Zugriff

    TRAIN TRAFFIC AUTOMATED CONTROL SYSTEM

    LESUN ANATOLIJ FEDOROVICH / RJABKOV ALEKSANDR NIKOLAEVICH / EFREMOV SERGEJ VLADIMIROVICH et al. | Europäisches Patentamt | 2016

    Freier Zugriff

    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


    Logic verification of Collision Avoidance System in train control systems

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