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.
Timed Specification Patterns for System Validation: A Railway Case Study
2011-01-01
14 pages
Aufsatz/Kapitel (Buch)
Elektronische Ressource
Englisch
Timed Specification Patterns for System Validation: A Railway Case Study
British Library Conference Proceedings | 2011
|Europäisches Patentamt | 2020
|The fastest timed railway run in Europe
Engineering Index Backfile | 1902
|