Résumé:
Dwyer et al. ont proposé des patrons de spécification qualitatives qui permettent aux
praticiens des outils de model-checking d’écrire des spécifications formelles principalement
utilisées pour le model-checking automatique. Bien que cela implique des formalismes qui
ne sont pas toujours faciles à manipuler par les ingénieurs, plusieurs techniques et langages
ont été proposés pour faciliter l’intégration des méthodes formelles basées sur ces patrons de
définition dans le domaine industriel. Cette thèse étudie un langage de description spécifique
nommé CDL qui aide les non-experts à écrire des spécifications formelles d’une manière plus
facile. Dans CDL, une propriété est transformée en un automate observateur pour effectuer
une analyse d’accessibilité. Les patrons CDL existants permettent aux non-experts de raisonner
sur l’occurrence et l’ordre des événements, mais pas suffisamment sur leur timing. De plus,
la sémantique des patrons et des transformations n’est pas idéalement formalisée et reste
complexe à comprendre et à utiliser. Enfin, l’exactitude des transformations des patrons aux
observateurs proposées n’a pas été prouvée. Ce travail a pour but d’étendre le système CDL
existant avec des patrons temporels ainsi que de formaliser la sémantique de ces patrons. En
outre, de nouvelles règles de transformation sont définies et leur exactitude est prouvée à l’aide
d’un outil de démonstration de théorèmes appelé Coq.
La contribution est illustrée sur un système industriel embarqué impliquant des navires
autonomes. Les navires autonomes doivent adhérer aux règles du trafic maritime pour assurer la
sécurité du trafic et réduire la responsabilité des fabricants. Cependant, les systèmes autonomes
ne peuvent évaluer le respect des règles que si elles sont formulées de manière précise et
mathématique. Dans cette thèse, nous formalisons les règles de trafic maritime de la Convention
sur le Règlement International pour Prévenir les Collisions en Mer (COLREGS) en utilisant nos
patrons de propriétés et les automates observateurs. En particulier, nous définissons les règles
de prévention des collisions entre deux navires motorisés.
