Incorporating verification of liveness properties in 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 automated technique which can be used in stages to derive the overall behaviour of a distributed program based on its architecture. CRA is particularly suitable for the analysis of programs which are subject to evolutionary change. When a program evolves, only behaviours of those subsystems affected by the change need be re-evaluated. The technique however has a limitation. The properties available for analysis are constrained by the set of actions that remain globally observable. The liveness properties of subsystems which involve hidden actions may therefore not be analysed. In this paper, we extend compositional reachability analysis to check liveness properties of subsystems which may involve actions that are not globally observable. 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