Local Reasoning about Parametric and Reconfigurable Component-based Systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2019

Local Reasoning about Parametric and Reconfigurable Component-based Systems

Marius Bozga
Radu Iosif
  • Fonction : Auteur
  • PersonId : 840083
Joseph Sifakis
  • Fonction : Auteur
  • PersonId : 857859

Résumé

We introduce a logical framework for the specification and verification of component-based systems, in which finitely many component instances are active, but the bound on their number is not known. Besides specifying and verifying parametric systems, we consider the aspect of dynamic reconfiguration, in which components can migrate at runtime on a physical map, whose shape and size may change. We describe such para-metric and reconfigurable architectures using resource logics, close in spirit to Separation Logic, used to reason about dynamic pointer structures. These logics support the principle of local reasoning, which is the key for writing modular specifications and building scalable verification algorithms, that deal with large industrial-size systems.
Fichier principal
Vignette du fichier
draft.pdf (306.93 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-02267423 , version 1 (19-08-2019)

Identifiants

  • HAL Id : hal-02267423 , version 1

Citer

Marius Bozga, Radu Iosif, Joseph Sifakis. Local Reasoning about Parametric and Reconfigurable Component-based Systems. 2019. ⟨hal-02267423⟩
26 Consultations
32 Téléchargements

Partager

Gmail Facebook X LinkedIn More