Compositional verification for component-based systems and application

The authors present a compositional method for the verification of component-based systems described in a subset of the behaviour-interaction- priority language encompassing multi-party interaction without data transfer. The method is based on the use of two kinds of invariants. Component invariants are over-approximations of components' reachability sets. Interaction invariants are global constraints on the states of components involved in interactions. The method has been implemented in the D-Finder tool and has been applied for checking deadlock-freedom. The experimental results on non-trivial examples show that this method allows either to prove deadlock-freedom or to identify very few deadlock configurations that can be analysed by using state-space exploration. © 2010 The Institution of Engineering and Technology.


Published in:
IET Software, 4, 3, 181 - 193
Year:
2010
ISSN:
17518806
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)