A Port Graph Calculus for Autonomic Computing and Invariant Verification

Oana Andrei 1 Helene Kirchner 2, *
* Auteur correspondant
2 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this paper, we first introduce port graphs as graphs with multiple edges and loops, with nodes having explicit connection points, called ports, and edges attaching to ports of nodes. We then define an abstract biochemical calculus that instantiates to a rewrite calculus on these graphs. Rules and strategies are themselves port graphs, i.e. first-class objects of the calculus. As a consequence, they can be rewritten as well, and rules can create new rules, providing a way of modeling adaptive systems. This approach also provides a formal framework to reason about computations and to verify useful properties. We show how structural properties of a modeled system can be expressed as strategies and checked for satisfiability at each step of the computation. This provides a way to ensure invariant properties of a system. This work is a contribution to the formal specification and verification of adaptive systems and to theoretical foundations ofautonomic computing.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

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

Contributeur : Helene Kirchner <>
Soumis le : dimanche 20 septembre 2009 - 12:48:22
Dernière modification le : jeudi 11 janvier 2018 - 06:22:10
Archivage à long terme le : mardi 15 juin 2010 - 23:55:45


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00418560, version 1



Oana Andrei, Helene Kirchner. A Port Graph Calculus for Autonomic Computing and Invariant Verification. TERMGRAPH 2009, 5th International Workshop on Computing with Terms and Graphs, Satellite Event of ETAPS 2009, A. Corradini, Mar 2009, York, United Kingdom. ⟨inria-00418560⟩



Consultations de la notice


Téléchargements de fichiers