Compositional Verification of Concurrent Systems by Combining Bisimulations - Inria - Institut national de recherche en sciences et technologies du numérique
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Conference Papers Year : 2019
Compositional Verification of Concurrent Systems by Combining Bisimulations
1 CONVECS - Construction of verified concurrent systems (Centre de recherche Inria 655 avenue de l'Europe 38330 Montbonnot Saint-Martin - France)
"> CONVECS - Construction of verified concurrent systems
2 CNR | ISTI - CNR Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo” [Pisa] (Institute of Information Science and Technologies 'Alessandro Faedo | Area della Ricerca CNR, via G. Moruzzi 1, I-56124 Pisa - Italy)
"> CNR | ISTI - CNR Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo” [Pisa]

Abstract

One approach to verify a property expressed as a modal μ-calculus formula on a system with several concurrent processes is to build the underlying state space compositionally (i.e., by minimizing and recomposing the state spaces of individual processes, keeping visible only the relevant actions occurring in the formula), and check the formula on the resulting state space. It was shown previously that, when checking the formulas of the Lμ-dsbr fragment of μ-calculus (consisting of weak modalities only), individual processes can be minimized modulo divergence-preserving branching (divbranching) bisimulation. In this paper, we refine this approach to handle formulas containing both strong and weak modalities, so as to enable a combined use of strong or divbranching bisimulation minimization on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend Lμ-dsbr with strong modalities and show that the combined minimization approach preserves the truth value of formulas of the extended fragment. We implemented this approach on top of the CADP verification toolbox and demonstrated how it improves the capabilities of compositional verification on realistic examples of concurrent systems.
Fichier principal
Vignette du fichier
main.pdf (521.12 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

hal-02295459 , version 1 (24-09-2019)
Identifiers

Cite

Frédéric Lang, Radu Mateescu, Franco Mazzanti. Compositional Verification of Concurrent Systems by Combining Bisimulations. FM 2019 - 23rd International Conference on Formal Methods, Oct 2019, Porto, Portugal. pp.196-213, ⟨10.1007/978-3-030-30942-8_13⟩. ⟨hal-02295459⟩
235 View
230 Download

Altmetric

Share

More