Abstract The aim of the work discussed in this paper is to introduce a method for verifying temporal requirements of time-constrained systems. The method predates by establishing a generic repository of observation patterns relative to a new time constraint taxonomy that we define. The method allows the automated verification of temporal requirements, initially expressed in a semi-formal formalism -UML State Machines (SM) with time annotations- through model transformation and model-checking technique. In practice, in order to check the temporal aspects of a given specification, the observation patterns relative to the extracted requirements are instantiated to obtain appropriate observers. Then, using a transformation algorithm, the system specification as well as the obtained observers are translated into Timed Automata (TA) models. Thereby, the verification is reduced to a reachability analysis within the global model bringing together the system under study and the obtained observers.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Timed Specification Patterns for System Validation: A Railway Case Study


    Beteiligte:
    Mekki, Ahmed (Autor:in) / Ghazel, Mohamed (Autor:in) / Toguyéni, Armand (Autor:in)


    Erscheinungsdatum :

    2011-01-01


    Format / Umfang :

    14 pages





    Medientyp :

    Aufsatz/Kapitel (Buch)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch




    Timed Specification Patterns for System Validation: A Railway Case Study

    Mekki, A. / Ghazel, M. / Toguyeni, A. | British Library Conference Proceedings | 2011



    The fastest timed railway run in Europe

    Rous-Marten, Charles | Engineering Index Backfile | 1902



    Runtime Verification of Railway Interlocking Software with Parametric Timed Automata

    Chai, Ming / Wang, Haifeng / Zhang, Jian et al. | IEEE | 2018