Checking and correcting safety 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 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 the 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. Properties involving actions encapsulated by subsystems may therefore not be analyzed. In this paper, we enhance the CRA technique to check safety properties which may contain actions that are not globally observable. To achieve this, the state machine model is augmented with a special trap state labelled as \pi. We propose a scheme to transform in stages a property that involves hidden actions to one that involves only globally observable actions. The enhanced technique also includes a mechanism aiming at reducing the debugging effort. The technique is illustrated using a case study of a gas station system