Context constraints for automated compositional reachability analysis

Behaviour analysis of complex concurrent systems has led to the search for enhanced reachability analysis techniques which support modularity and which control the state explosion problem. While modularity has been achieved, state explosion is still a problem. Indeed, this problem may even be exacerbated as a locally minimised subsystem may contain many states and transitions forbidden by its environment or context. Context constraints, specified as interface processes, are restrictions imposed by the environment on subsystem behaviour. Recent research has suggested that the state explosion problem can be effectively controlled if context constraints are incorporated in compositional reachability analysis (CRA). Although theoretically very promising, the approach has been rarely used in practice because it generally requires a more complex computational model and the context constraints need to be specified. This paper presents a technique to automate the approach while using the same computational model as CRA. Context constraints are derived automatically, based on a set of sufficient conditions for these constraints to be transparently included when building reachability graphs. As a result, the global reachability graph generally using our technique is shown to be observationally equivalent to that generated by CRA without the inclusion of context constraints. The technique is illustrated with a clients/server system