Skip to Main content Skip to Navigation
Conference papers

Sound Verification Procedures for Temporal Properties of Infinite-State Systems

Abstract : 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.
Complete list of metadata

https://hal.archives-ouvertes.fr/hal-03243129
Contributor : David Chemouil Connect in order to contact the contributor
Submitted on : Friday, June 4, 2021 - 3:47:05 PM
Last modification on : Wednesday, July 21, 2021 - 5:02:35 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03243129, version 2

Citation

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⟩

Share

Metrics

Record views

83

Files downloads

57