Contribution à la Spécification et à la Vérification des Exigences Temporelles - Proposition d?une extension des SRS d?ERTMS niveau 2

Due to the increasing complexity of today?s industrial systems in the railway domain, requirements' engineering has become a major issue in the development cycle of such systems. The work developed in this thesis aims at assisting the engineering process of temporal requirements for time-constrained complex systems. Our contributions concern three phases: the specification, the behavioural modelling and the verification. For the specification of temporal requirements, a new temporal property typology taking into account all the common requirements one may meet when dealing with requirements specification, is introduced. Then, to facilitate the expression and the identification, we have proposed a structured English grammar (SEG). Concretely, each assertion generated through our grammar describes one temporal property and serves as a handler that aids expressing and understanding the requirement. Nevertheless, even if each requirement taken individually is correct, we have no guarantee that a set of temporal properties one may express is consistent. Here we have proposed an algorithm based on graph theory techniques to check the consistency of temporal requirements sets. For the behaviour modelling, we have proposed an algorithm for transforming UML State Machine with time annotations into Timed Automata (TA). The idea is to allow the user manipulating a quite intuitive notation (UML SM diagrams) during the modelling phase and thereby, automatically generate formal models (TA) that could be used directly by the verification process. The transformation rules have been defined at the SM and TA meta-models level. Furthemore, a formal semantics has been defined for each of these models (SM and TA). Finally, our transformation algorithm was validated while prooving a strong temporal bisimulation relationship between the source model and the target model. Finally, for the verification phase, we have adopted an observer-based technique. Actually, we have developped a repository of observation patterns where each pattern is relative to a particular temporal requirement class in our classification. In practice, in order to check the temporal requirements of a given model, the observation patterns relative to the investigated properties are instantiated to make appropriate TA observers. Then using our transformation algorithm, the system model (denoted in the shape of a UML SM model with time annotations) is translated into TA models. The TA system model is next synchronized with the TA observers. Thereby, the verification process is reduced to a reachability analysis of the observers? KO states relative to the requirements? violation. The whole of the developed mechanisms have been implemented in prototype software tools. The last part of our work is a proposal for the integration of level crossings (LC) into the specifications of the European railway control and signalling system, ERTMS. This case study has been used to illustrate the various contributions developed in this thesis.

  • Authors:
    • MEKKI, Ahmed
  • Publication Date: 2012


  • French

Media Info

  • Media Type: Digital/other
  • Pagination: 177

Subject/Index Terms

Filing Info

  • Accession Number: 01493059
  • Record Type: Publication
  • Source Agency: Institut Francais des Sciences et Technologies des Transports, de l'Aménagement et des Réseaux (IFSTTAR)
  • Files: ITRD
  • Created Date: Sep 17 2013 11:41AM