Checking deadlock-freedom of parametric component-based systems - IMAG Accéder directement au contenu
Article Dans Une Revue Journal of Logical and Algebraic Methods in Programming Année : 2020

Checking deadlock-freedom of parametric component-based systems

Marius Bozga
Radu Iosif
Joseph Sifakis
  • Fonction : Auteur
  • PersonId : 1084330

Résumé

We propose an automated method for computing inductive invariants used to proving deadlock freedom of parametric component-based systems. The method generalizes the approach for computing structural trap invariants from bounded to parametric systems with general architectures. It symbolically extracts trap invariants from interaction formulae defining the system architecture. The paper presents the theoretical foundations of the method and proves its soundness. It also reports on a preliminary experimental evaluation on several textbook examples.
Fichier principal
Vignette du fichier
submission.pdf (533.67 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03040227 , version 1 (14-12-2020)

Identifiants

Citer

Marius Bozga, Radu Iosif, Joseph Sifakis. Checking deadlock-freedom of parametric component-based systems. Journal of Logical and Algebraic Methods in Programming, 2020, 119, pp.100621. ⟨10.1016/j.jlamp.2020.100621⟩. ⟨hal-03040227⟩
23 Consultations
62 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More