Sound Verification Procedures for Temporal Properties of Infinite-State Systems - Assistance à la Certification d’Applications DIstribuées et Embarquées Accéder directement au contenu
Communication Dans Un Congrès Année : 2021

Sound Verification Procedures for Temporal Properties of Infinite-State Systems

Résumé

First-Order Linear Temporal Logic (FOLTL) is particularly convenient to specify distributed systems, in particular because of the unbounded aspect of their state space. We have recently exhibited novel decidable fragments of FOLTL which pave the way for tractable verification. However, these fragments are not expressive enough for realistic specifications. In this paper, we propose three transformations to translate a typical FOLTL specification into two of its decidable fragments. All three transformations are proved sound (the associated propositions are proved in Coq) and have a high degree of automation. To put these techniques into practice, we propose a specification language relying on FOLTL, as well as a prototype which performs the verification, relying on existing model checkers. This approach allows us to successfully verify safety and liveness properties for various specifications of distributed systems from the literature.
Fichier principal
Vignette du fichier
main.pdf (912.57 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03243129 , version 1 (31-05-2021)
hal-03243129 , version 2 (04-06-2021)

Identifiants

  • HAL Id : hal-03243129 , version 2

Citer

Quentin Peyras, Jean-Paul Bodeveix, Julien Brunel, David Chemouil. Sound Verification Procedures for Temporal Properties of Infinite-State Systems. 33rd International Conference on Computer-Aided Verification (CAV 2021), Jul 2021, Los Angeles (Online), United States. ⟨hal-03243129v2⟩
191 Consultations
195 Téléchargements

Partager

Gmail Facebook X LinkedIn More