Sémantique formelle des observateurs pour la validation des transformations

Abstract

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.