Ensuring Reachability by Design

Benoit Caillaud 1 Jean-Baptiste Raclet 2
1 S4 - System synthesis and supervision, scenarios
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
2 ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
IRIT - Institut de recherche en informatique de Toulouse
Résumé : Les méthodes de conception modulaire procèdent par décomposition d'un système en un ensemble de composants qui seront, dans un premier temps, réalisés indépendamment les uns des autres, pour être par la suite combinés de façon à former un système complet. Il est alors utile d'associer aux composants des interfaces qui servent à abstraire les détails de réalisation, tout en exposant les aspects cruciaux concernant les interactions avec les autres composants et l'environnement. Alors que l'état de l'art sur les interfaces concerne en premier lieu l'implémentation indépendante de propriétés de sureté, ce rapport porte sur la prise en compte de propriétés d'atteignabilité, qui sont en général non compositionnelles. L'approche défendue ici consiste 'a contrôler le flot de conception d'un systèmes, c'est 'a dire, l'évolution des interfaces tout au long des étapes de composition et de raffinement, de telle manière qu'une propriété d'atteignabilité est garantie par construction. Les spécifications modales sont reconnues comme un formalisme d'interface approprié. Elles sont ici étendues par ajout de marquage des états, servant a modéliser l'atteignabilité de certains états. L'algèbre d'interfaces modales marquée, avec ses opérateurs de composition logique et structurelle, permet d'assurer par construction l'atteignabilité de certains états.
Type de document :
Rapport
[Research Report] RR-7928, INRIA. 2012, pp.20
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00696151
Contributeur : Benoît Caillaud <>
Soumis le : vendredi 11 mai 2012 - 09:27:11
Dernière modification le : jeudi 11 janvier 2018 - 06:27:06
Document(s) archivé(s) le : jeudi 15 décembre 2016 - 05:43:14

Fichier

rapport.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00696151, version 1

Citation

Benoit Caillaud, Jean-Baptiste Raclet. Ensuring Reachability by Design. [Research Report] RR-7928, INRIA. 2012, pp.20. 〈hal-00696151〉

Partager

Métriques

Consultations de la notice

659

Téléchargements de fichiers

127