en fr Contribution for the Specification and the Verification of Temporal Requirements : Proposal of an extension for the ERTMS-Level 2 specifications Contribution à la Spécification et à la Vérification des Exigences TemporeReportar como inadecuado




en fr Contribution for the Specification and the Verification of Temporal Requirements : Proposal of an extension for the ERTMS-Level 2 specifications Contribution à la Spécification et à la Vérification des Exigences Tempore - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 LAGIS - Laboratoire d-Automatique, Génie Informatique et Signal

Abstract : 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

Résumé : Les travaux développés dans cette thèse visent à assister le processus d’ingénierie des exigences temporelles pour les systèmes complexes à contraintes de temps. Nos contributions portent sur trois volets : la spécification des exigences, la modélisation du comportement et la vérification. Pour le volet spécification, une nouvelle classification des exigences temporelles les plus communément utilisées a été proposée. Ensuite, afin de cadrer l’utilisateur durant l’expression des exigences, une grammaire de spécification à base de motifs prédéfinis en langage naturel est développée. Les exigences générées sont syntaxiquement précises et correctes quand elles sont prises individuellement, néanmoins cela ne garantie pas la cohérence de l’ensemble des exigences exprimées. Ainsi, nous avons développé des mécanismes capables de détecter certains types d’incohérences entre les exigences temporelles. Pour le volet modélisation du comportement, nous avons proposé un algorithme de transformation des state-machine avec des annotations temporelles en des automates temporisés. L’idée étant de manipuler une notation assez intuitive et de générer automatiquement des modèles formels qui se prêtent à la vérification. Finalement, pour le volet vérification, nous avons adopté une technique de vérification à base d’observateurs et qui repose sur le model-checking. Concrètement, nous avons élaboré une base de patterns d’observation ou observateurs ; chacun des patterns développés est relatif à un type d’exigence temporelle dans la nouvelle classification. Ainsi, la vérification est réduite à une analyse d’accessibilité des états correspondants à la violation de l’exigence associée

en fr

Keywords : Temporal requirements System specification Model transformation Verification and validation Observation patterns Model-checking Railway control systems ERTMS

Mots-clés : Exigences temporelles Spécification Transformation de modèles Vérification et validation Observateur Contrôle-commande ferroviaire





Autor: Ahmed Mekki -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados