Compositional model checking is lively
| Autor: | de Putter, S.M.J., Wijs, A.J., Proença, J., Lumpe, M. |
|---|---|
| Přispěvatelé: | Software Engineering and Technology |
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
Model checking
Computer science Modulo Liveness 020207 software engineering Context (language use) 0102 computer and information sciences 02 engineering and technology Space (mathematics) 01 natural sciences Algebra Congruence (geometry) 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 0202 electrical engineering electronic engineering information engineering Equivalence relation Limit state design |
| Zdroj: | Formal Aspects of Component Software ISBN: 9783319680330 FACS Formal Aspects of Component Software: 14th International Conference, FACS 2017, Braga, Portugal, October 10-13, 2017, Proceedings, 117-136 STARTPAGE=117;ENDPAGE=136;TITLE=Formal Aspects of Component Software |
| ISSN: | 0302-9743 |
| Popis: | Compositional model checking approaches attempt to limit state space explosion by iteratively combining behaviour of some of the components in the system and reducing the result modulo an appropriate equivalence relation. For an equivalence relation to be applicable, it should be a congruence for parallel composition where synchronisations between the components may be introduced. An equivalence relation preserving both safety and liveness properties is divergence-preserving branching bisimulation (DPBB). It is generally assumed that DPBB is a congruence for parallel composition, even in the context of synchronisations between components. However, so far, no such results have been published. This work finally proves that this is the case. Furthermore, we discuss how to safely decompose an existing LTS network in components such that the re-composition is equivalent to the original LTS network. All proofs have been mechanically verified using the Coq proof assistant. Finally, to demonstrate the effectiveness of compositional model checking with intermediate DPBB reductions, we discuss the results we obtained after having conducted a number of experiments. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|