Contribution for the Specification and the Verification of Temporal Requirements : Proposal of an extension for the ERTMS-Level 2 specifications
type: Dataset
description: The work developed in this thesis aims to assist the engineering process of temporal requirements for time-constrained complex systems. Our contributions concern three phases: the specification, the behaviour modelling and the verification. For the specification of temporal requirements, a new temporal properties typology taking into account all the common requirements one may meet when dealing with requirements specification, is introduced. Then, to facilitate the expression, we have proposed a structured English grammar. 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 diagramsduring the modelling phase and thereby, automatically generate formal models (TA) that could be used directly by the verification process. Finally, for the verification phase, we have adopted an observer-based technique. Actually, we have developed a repository of observation patterns where each pattern is relative to a particular temporal requirement class in our classification. Thereby, the verification process is reduced to a reachability analysis of the observers’ KO states relatives to the requirements’ violation
identifier: NNT: 2012ECLI0006
issued: 2026-05-15T14:27:04.773969
language: fr
modified: 2026-05-15T14:27:04.773975
contact point: Organization
  fn: CCSD
keyword: controlecommande-ferroviaire
keyword: ertms
keyword: exigences-temporelles
keyword: infoeu-reposemanticsdoctoralthesis
keyword: model-checking
keyword: model-transformation
keyword: observateur
keyword: observation-patterns
keyword: railway-control-systems
keyword: specification
keyword: spiotherengineering-sciences-physicsother
keyword: system-specification
keyword: temporal-requirements
keyword: theses
keyword: transformation-de-modeles
keyword: verification-and-validation
keyword: verification-et-validation
landing page: https://theses.hal.science/tel-00710674

Contribution for the Specification and the Verification of Temporal Requirements : Proposal of an extension for the ERTMS-Level 2 specifications
type: Distribution
format: HTML
issued: 2026-05-15T14:27:04.846979
modified: 2026-05-15T14:27:04.735359
access URL: https://theses.hal.science/tel-00710674

test_moissonnage_selune
type: Agent