Compositional reachability analysis of finite-state distributed systems with user-specified constraints

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. This staged composition may however exacerbate the state explosion problem. A promising way to alleviate this problem is to include, in the analysis of each subsystem, the behaviour constraints imposed by its environment. Behaviour constraints can be derived algorithmically but may be too weak to adequately constrain the compositional analysis. In this paper, we describe a technique which enables software developers to also specify behaviour constraints intuitively. These constraints can be combined with those derived algorithmically. As constraints specified by software developers may be incorrect, the technique incorporates an effective mechanism to detect incorrect constraints and give an indication of how to correct them. Incorporation of the mechanism does not increase the complexity of analysis. The mechanism is supported by augmenting the state machine model with a special state *. The state is used to capture automatically potential errors in the constraints specified by software developers. The mechanism can also be utilised to detect violation of design assumptions. A gas station system is used as a case study in our discussion