Sémantique formelle des observateurs pour la validation des transformations

Abstract

Dwyer et al. ont proposé des patrons de spéci￿cation qualitatives qui permettent aux praticiens des outils de model-checking d’écrire des spéci￿cations 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éci￿que nommé CDL qui aide les non-experts à écrire des spéci￿cations formelles d’une manière plus facile. Dans CDL, une propriété est transformée en un automate observateur pour e￿ectuer 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 su￿samment 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. En￿n, 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 tra￿c maritime pour assurer la sécurité du tra￿c 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 tra￿c 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.