A parametric verification tool for distributed concurrent systems

In the recent past, many verification tools for distributed concurrent system, which are based on process description languages, have been proposed (for a detailed survey see [15]). Any of these existing tools is based on a specific theory and, therefore, it is suitable for analisying a particular class of problems. In particular, all the existing tools are based on the so-called interleaving models. This implies that only the actions of a communicating system, and their temporaI ordering, can be studied. Therefore, such tools are adequate only for the final user of a concurrent system, that is only interested in the outputs of the execution of a process. Indeed, the designer or the programmer of a distributed system, that is strongly interested in the causal and/or spatial relation between events, does not have much help from the existing tools, i.e. he/she needs more information than the one provided by these tools. The concurrency models which would give much help to designers and programmers are the ones called true concurrent. In this paper we describe a tool which supports more than one concurrency model and which allows to simply switch from one model to the other. Roughly speaking, we describe a parametric tool that permits to observe many aspects of a distributed system. Among the others the temporal ordering of the events and their causal or spatial relation can be studied. An introduction to the general motivations and to the theory underlying our approach is given in [17].