Ensuring Reachability by Design - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2012

Ensuring Reachability by Design

Résumé

Modular design aims at decomposing systems as a set of distinct components that can be independently developed and then assembled all together. Interfaces are then attached to components; they abstract implementation details while exposing to the environment relevant information about cross-component interactions. Whereas state-of-the-art on interfaces essentially consider independent implementability of safety properties, we consider in this paper reachability properties, which are in general not compositional. The approach we advocate consists in controlling the design flow of components, that is, the evolution of their interfaces through combinations and refinements, in order to ensure a reachability property by construction. Modal specifications are widely acknowledged as a suitable specification formalism for interface- based design. In order to obtain the required expressivity, we extend them with marked states to model states to be reached. We then develop an algebra with both logical and structural composition operators ensuring reachability properties by design.
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.
Fichier principal
Vignette du fichier
rapport.pdf (765.34 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00696151 , version 1 (11-05-2012)

Identifiants

  • HAL Id : hal-00696151 , version 1

Citer

Benoit Caillaud, Jean-Baptiste Raclet. Ensuring Reachability by Design. [Research Report] RR-7928, INRIA. 2012, pp.1-20. ⟨hal-00696151⟩
217 Consultations
190 Téléchargements

Partager

Gmail Facebook X LinkedIn More