LOGIN TO YOUR ACCOUNT

Username
Password
Remember Me
Or use your Academic/Social account:

CREATE AN ACCOUNT

Or use your Academic/Social account:

Congratulations!

You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.

Important!

Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message

CREATE AN ACCOUNT

Name:
Username:
Password:
Verify Password:
E-mail:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Languages: French
Types: Article
Subjects: Modularité, Spécification formelle, Vérification et validation, Logique temporelle, Théorie des catégories, Télécommunications, Systèmes embarqués, 000, Modularity, Formal specification, Verification and validation, Temporal logic, Category theory, Telecommunications, Embedded systems
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. 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.
  • No references.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article