Sémantique formelle des observateurs pour la validation des transformations - Baroudi, Djamila (l’Université de Mostaganem, 2022)
Dwyer et al. ont proposé des patrons de spécication qualitatives qui permettent aux praticiens des outils de model-checking d’écrire des spécications 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énition dans le domaine industriel. Cette thèse étudie un langage de description spécique nommé CDL qui aide les non-experts à écrire des spécications formelles d’une manière plus facile. Dans CDL, une propriété est transformée en un automate observateur pour eectuer 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 susamment 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. Enn, 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énies 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 trac maritime pour assurer la sécurité du trac 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 trac 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énissons les règles de prévention des collisions entre deux navires motorisés.
Keywords: Patrons de propriétés, Spécication des propriétés temporelles, Automates observateurs, Preuve de théorème, Validation des transformations, Navires autonomes