Timed Specification Patterns for System Validation. A railway case study
MEKKI ; GHAZEL ; TOGUYENI
Type de document
ARTICLE A COMITE DE LECTURE NON REPERTORIE DANS BDI (ACLN)
Langue
anglais
Auteur
MEKKI ; GHAZEL ; TOGUYENI
Résumé / 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.
Source
LNEE, Lecture Notes in Electrical Engineering, num. Vol 89, Part 2, p121-134 p.
Editeur
Springer
