Institut Français des Sciences et Technologies des Transports, de l'Aménagement et des Réseaux

Type de document

THESE

Langue

francais

Auteur

MEKKI

Résumé / Abstract

De par la complexité croissante des systèmes industriels de nos jours et notamment dans le secteur du transport ferroviaire, l’ingénierie des exigences est devenue un enjeu majeur dans le cycle de développement. Les travaux développés dans le cadre de 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, à savoir : la phase de spécification des exigences, la phase de modélisation du comportement et la phase de vérification. Pour le volet spécification, une nouvelle classification des exigences temporelles les plus communément utilisées a été proposée. Par la suite, afin d’assister et cadrer l’utilisateur lors de la phase d’expression des exigences, nous avons développé une grammaire de spécification à base de motifs pré-définis en langage naturel. Chaque assertion générée à partir de cette grammaire identifie une classe unique dans la classification des exigences (et vice-versa). Les exigences générées sont syntaxiquement précises et correctes quand elles sont prises individuellement, néanmoins cela ne garantit pas la cohérence de l’ensemble des exigences exprimées. Ainsi, afin de remédier à cette problématique de cohérence, nous avons développé des mécanismes capables de détecter certains types d’incohérences entre les exigences temporelles. Ces mécanismes sont basés sur une reformulation des exigences sous forme d'un graphe orienté. Pour le deuxième volet, la modélisation du comportement, nous avons proposé un algorithme de transformation des state-machines (SM) avec des annotations temporelles en des automates temporisés (AT). L’idée étant de donner la possibilité à l’utilisateur de manipuler une notation assez intuitive (diagramme SM d’UML) lors de la phase de modélisation et d'en générer automatiquement des modèles formels (AT) qui se prêtent à la vérification. Les règles de transformation sont définies au niveau des méta-modèles respectifs des SM et des AT, que nous avons proposés. Par ailleurs, une sémantique formelle a été définie pour chacun de ces modèles. Enfin, notre algorithme de transformation a été validé par la démonstration d’une relation de bisimulation temporelle forte entre le modèle source et le modèle cible. Finalement, pour la phase de vérification, nous avons adopté une technique de vérification à base d’observateurs et qui repose sur le model-checking. Concrètement, en se basant sur la classification des exigences temporelles que nous avons développée, nous avons élaboré une base de patterns d’observation ; chacun des patterns développés est relatif à un type d’exigence temporelle. Concrètement, pour chaque classe d’exigence dans notre classification, le pattern observateur associé correspond à un modèle automate temporisé paramétrable dont les instances jouent le rôle de “chien de garde” (ou watchdog en anglais) pour surveiller les exigences de cette classe. Ainsi, la vérification est réduite à une analyse d’accessibilité des états d’erreur, états correspondant à la violation de l’exigence associée. Il est à noter par ailleurs que des prototypes logiciels ont été développés pour supporter les différents mécanismes proposés. La dernière partie de nos travaux concerne une proposition d’extension des spécifications du système de contrôle-commande et de signalisation ferroviaire, ERTMS, afin d’y intégrer les passages à niveau. Ce cas d’étude nous a servi à l’illustration des différentes contributions proposées dans cette thèse.