|
HKUST Institutional Repository >
Computer Science and Engineering >
CSE Conference Papers >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1783.1/2111
|
| Title: | Verification of liveness properties using compositional reachability analysis |
| Authors: | Cheung, Shing-Chi
Giannakopoulou, Dimitra
Kramer, Jeff |
| Keywords: | Reachability analysis
Compositional verification
Distributed computing systems
Labelled transition systems
Büchi automata
Liveness properties |
| Issue Date: | Nov-1997 |
| Citation: | ACM. Sigsoft Software Engineering Notes, v. 22, no. 6, Nov. 1997, p. 227-43 |
| Abstract: | 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 simultaneous checking of multiple properties (both liveness and safety), and identifies those properties that are violated. The effectiveness of the extended technique is illustrated using a case study of a Reliable Multicast Transport Protocol (RMTP) with over 96,000 states and 660,000 transitions. |
| Rights: | © ACM, 1997. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM. Sigsoft Software Engineering Notes, {vol. 22, no. 6, (November 1997)} |
| URI: | http://hdl.handle.net/1783.1/2111 |
| Appears in Collections: | CSE Conference Papers
|
Files in This Item:
| File |
Description |
Size | Format |
|---|
| 1_8veri.pdf | pre-published version | 1441Kb | Adobe PDF | View/Open |
|
All items in this Repository are protected by copyright, with all rights reserved.
|
