The safety of control systems are becoming increasingly important as computers pervade them on which human life depends. In rail transportation fields, this has become more complex and the methods to ensure the correctness of train control system have been slow in development. The failure to meet time deadline can have serious or even fatal consequences. This paper presents a new method for performing this verification task. In the proposed method the real-time system is modeled by Timed Automata Network (TAN) and verified by model checking which explores the state space to determine whether the system satisfies a given specification. The case study of ATP (Automatic Train Protection) shows how the method can assist in designing more efficient and reliable real-time systems. Firstly, the state transitions and multi-tasks ATP onboard model will be modeled with Timed Automata Network (TAN) model, and then the time sequences of each task are expressed in UML Sequence Diagrams. Finally, the timing characteristics will be verified to meet the requirement by SMV model checker. A major conclusion of the survey is that formal methods, while still immature in some respects, can be used successfully to model and verify real-time concurrent systems.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formal modeling and verification of real-time concurrent systems


    Beteiligte:
    Yan, Fei (Autor:in) / Tang, Tao (Autor:in)


    Erscheinungsdatum :

    2008


    Format / Umfang :

    6 Seiten, 6 Quellen



    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch






    Formal Verification for the Development and Real-Time Application of Autonomous Systems

    NADERHIRN MICHAEL | Europäisches Patentamt | 2022

    Freier Zugriff

    Modeling, analysis and verification of real-time resource access control protocols: a formal approach

    Hazra, Rumpa / Dey, Shouvik / Singha, Jayashree | British Library Online Contents | 2018


    Semantically enhanced containers for concurrent real-time systems

    Dechev, D. / Pirkelbauer, P. / Rouquette, N. et al. | Tema Archiv | 2009