Compositional verification for component-based systems and application

We present a compositional method for the verification of component-based systems described in a subset of the BIP language encompassing multi-party interaction without data transfer. The method is based on the use of two kinds of invariants. Component invariants which are over-approximations of components' reachability sets. Interaction invariants which are constraints on the states of components involved in interactions. Interaction invariants are obtained by computing traps of finite-state abstractions of the verified system. The method is applied for deadlock verification in the D-Finder tool. D-finder is an interactive tool that takes as input BIP programs and applies proof strategies to eliminate potential deadlocks by computing increasingly stronger invariants. The experimental results on non-trivial examples allow either to prove deadlock-freedom or to identify very few deadlock configurations that can be analyzed by using state space exploration.


Published in:
Automated Technology for Verification and Analysis. Proceedings 6th International Symposium, ATVA 2008, 64 - 79
Presented at:
Automated Technology for Verification and Analysis. Proceedings 6th International Symposium, ATVA 2008, Berlin, Germany
Year:
2008
Keywords:
Laboratories:




 Record created 2013-03-14, last modified 2018-03-17

n/a:
Download fulltext
PDF

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)