Checking subsystem safety properties in compositional reachability analysis

The software architecture of a distributed system can be described as a hierarchical composition of subsystems, with interacting processes as the leaves of the hierarchy. Process behaviour can be specified using finite-state machines. A global state machine describing the overall system behaviour can be constructed using compositional reachability analysis techniques. These techniques compose the global state machine of a system from its component processes in stages, based on the specified hierarchy. The key to the success of these analysis techniques is to employ a modular software architecture and hide as many internal actions as possible in each subsystem. A subsystem containing fewer observable actions can generally be represented by a simpler state machine. However, the properties that are available for reasoning (analysis) in the global state machine are constrained by the set of remaining globally observable actions. In this paper, we introduce a technique to check safety properties of subsystems which may contain actions that are not globally observable. We have found that these safety properties can still be checked in the framework of a compositional reachability analysis technique. Our technique is supported by augmenting the state machine model with a special state 'pi'. The state is used to capture possible violation of the safety properties specified by software developers. In the paper, safety properties are expressed using finite-state machines and concepts are illustrated using a gas station system as a case study