Timed Specification Patterns for System Validation. A railway case study

International audienceThe 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