Sciweavers

Share
ESEC
1997
Springer

Verification of Liveness Properties Using Compositional Reachability Analysis

9 years 2 months ago
Verification of Liveness Properties Using Compositional Reachability Analysis
The software architecture of a distributed program can be represented by a hierarchical composition of subsystems, with interacting processes at the leaves of the hierarchy. Compositional reachability analysis (CRA) is a promising state reduction technique which can be automated and used to derive in stages the overall behaviour of a distributed program based on its architecture. Conventional CRA however has a limitation. The properties available for analysis after composition and reduction are constrained by the set of actions that remain globally observable. The liveness properties which involve internal actions of subsystems may therefore not be analysed. In this paper, we extend compositional reachability analysis to check liveness properties which may involve actions that are not globally observable. In particular, our approach permits the hiding of actions independently of the liveness properties that are to be verified in the final graph. In addition, it supports the simultaneo...
Shing-Chi Cheung, Dimitra Giannakopoulou, Jeff Kra
Added 07 Aug 2010
Updated 07 Aug 2010
Type Conference
Year 1997
Where ESEC
Authors Shing-Chi Cheung, Dimitra Giannakopoulou, Jeff Kramer
Comments (0)
books