The tracta approach for behaviour analysis of concurrent systems

The need for modularity in the behaviour analysis of concurrent systems has been answered successfully by making reachability analysis compositional. Compositional reachability analysis (CRA) on the other hand, often exacerbates the state explosion problem; subsystem analysis leaves out information from the subsystem environment (context), which could considerably reduce the number of states allowed into its b ehaviour state-graph. To deal with that, we have chosen to incorp orate context constraints in CRA. In the Tracta approach develop ed in our section, context constraints are expressed as pro cesses in our mo del (we call them interface rocesses), that are composed with the subsystem, without affecting the global system behaviour. Tracta supports both automatically generated and user-specied interfaces. It also provides an elegant way of checking violation of safety properties by the system under analysis. This work, besides introducing the main open problems in this area of research, is a detailed presentation of Tracta and its underlying theory, in their current form