Modularité pour la conception et la validation formelles de systèmes Wiels, Virginie 1997-10-02 Ecole Nationale Supérieure de l'Aéronautique et de l'Espace

Directeur(s) de thèse:  Michel, Pierre Laboratoire :  Département d’Etudes et de Recherches en Informatique -DERI Classification : Informatique

Accès :  Texte intégral Mots-clés : Modularité, Spécification formelle, Vérification et validation, Logique temporelle, Théorie des catégories, Télécommunications, Systèmes embarqués Résumé : Structuration et compositionnalité sont des besoins importants dans le domaine des techniques formelles pour maîtriser la taille et la complexité des spécifications. Nous proposons un formalisme qui permet de spécifier des systèmes de façon modulaire, mais aussi d'exploiter la structure des spécifications pour réaliser des vérifications modulaires. Un outil de spécification (Moka) est associé a ce formalisme et peut être combiné avec des outils de démonstration logique existants. L’approche est illustrée sur trois applications de domaines différents. Nous mettons d’abord l'accent sur les besoins d'un cadre à la fois structuré, expressif et qui permette d'utiliser des outils de vérification et de validation. Pour répondre à ces besoins, nous proposons de combiner la logique temporelle (pour l’expressivité et les outils de vérification) avec des techniques algébriques (pour la structuration). Nous présentons ensuite l'approche qui combine le calcul de modules défini par Ehrig et Mahr avec une logique temporelle. Elle s'appuie sur les travaux de Fiadeiro et Maibaum utilisant la théorie des catégories pour leur "Object Calculus". L’outil associé utilise les aspects constructifs de la théorie des catégories pour mettre en œuvre les modules de spécification et les opérations de composition. L'approche est illustrée par une application au domaine des télécommunications. Les aspects vérification sont enfin abordés: nous expliquons comment le formalisme peut être utilisé pour faire de la vérification modulaire et l'intérêt d'interfacer l’outil Moka avec un outil de démonstration logique (ici TRIO). Deux autres applications sont présentées: un mécanisme de tolérance aux fautes et un système de contrôle de commandes d'avion. Résumé (anglais) : Structuration and compositionality are important needs in the formal technique field in order to master specification size and complexity. We propose a formalism that allows to specify systems in a modular way, but also to exploit specification structure in order to realize modular verifications. A specification tool (Moka) is associated with this formalism and can be combined with existing demonstration tools. The approach is illustrated on three applications from different fields. We first focus on the needs for a framework that is at the same time structured, expressive and allowing use of verification and validation tools. To fulfill these requirements, we propose to combine temporal logic (for its expressivity and verification tools) and algebraic techniques (for its structuration capabilities). We then present the approach that combines Ehrig and Mahr module calculus and temporal logic. It is based on Fiadeiro and Maibaum works using category theory for their “Object Calculus”. The associated tool uses the constructive aspects of category theory to implement specification modules and composition operations. The approach is illustrated on a telecommunication application. The verification aspects are finally detailed: we described how the formalism can be used to make modular verification and we explain why interfacing Moka with a demonstration tool (TRIO here) is interesting. Two applications are presented: a fault-tolerance mechanism and an electrical flight control system. Langue : Français

Exporter au format XML