Timed Specification Patterns for System Validation. A railway case study

Mekki, Ahmed; Ghazel, Mohamed; Toguyeni, Armand

Document type :

Partie d'ouvrage: Chapitre

DOI :

10.1007/978-3-642-19539-6_8

Title :

Timed Specification Patterns for System Validation. A railway case study

Author(s) :

Mekki, Ahmed [Auteur correspondant]
Systèmes Tolérants aux Fautes [STF]
Ghazel, Mohamed [Auteur]
Évaluation des Systèmes de Transports Automatisés et de leur Sécurité [IFSTTAR/ESTAS]
Université de Lille, Sciences et Technologies
Toguyeni, Armand [Auteur]

Systèmes Tolérants aux Fautes [STF]

Scientific editor(s) :

Juan Andrade Cetto
Jean-Louis Ferrier
Joaquim Filipe

Book title :

Informatics in Control, Automation and Robotics, Lecture Notes in Electrical Engineering

Publisher :

Springer Berlin Heidelberg

Publication date :

2011

ISBN :

978-3-642-19538-9

HAL domain(s) :

Informatique [cs]/Automatique

English abstract : [en]

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 ...
Show more >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.Show less >

Language :

Anglais

Audience :

Internationale

Popular science :

Non

Collections :

Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL

Files

https://api.istex.fr/document/04954A42FDF2BB0E09C8A6D54A13FEA9ADE9C651/fulltext/pdf?sid=hal
Open access
Access the document

https://api.istex.fr/document/04954A42FDF2BB0E09C8A6D54A13FEA9ADE9C651/fulltext/pdf?sid=hal
Open access
Access the document

https://api.istex.fr/document/04954A42FDF2BB0E09C8A6D54A13FEA9ADE9C651/fulltext/pdf?sid=hal
Open access
Access the document

https://api.istex.fr/document/04954A42FDF2BB0E09C8A6D54A13FEA9ADE9C651/fulltext/pdf?sid=hal
Open access
Access the document

https://api.istex.fr/document/04954A42FDF2BB0E09C8A6D54A13FEA9ADE9C651/fulltext/pdf?sid=hal
Open access
Access the document

https://api.istex.fr/document/04954A42FDF2BB0E09C8A6D54A13FEA9ADE9C651/fulltext/pdf?sid=hal
Open access
Access the document

https://api.istex.fr/document/04954A42FDF2BB0E09C8A6D54A13FEA9ADE9C651/fulltext/pdf?sid=hal
Open access
Access the document

https://api.istex.fr/document/04954A42FDF2BB0E09C8A6D54A13FEA9ADE9C651/fulltext/pdf?sid=hal
Open access
Access the document

pdf
Open access
Access the document

fulltext.pdf
Open access
Access the document

Timed Specification Patterns for System ... BibTeX CSV Excel RIS

Files

Timed Specification Patterns for System ...

BibTeX

CSV

Excel

RIS