Automatizing parametric reasoning on distributed systems

There can be different views of a concurrent distributed system, depending on who observes it. The final user may just want to know how the system behaves in terms of its possible sequences of actions, while the designer may want to know what are the sequential components of a system or how are they distributed in space. In other words, there is not a widely accepted single semantic model for concurrent systems. This paper describes a parametric verification tool for process description languages. It performs a symbolic execution of processes at different levels of abstraction and verifies deadlock and reachability properties. The tool also provides facilities to check behavioural equivalences. In addition to the classical interleaving semantics, truly concurrent approaches based on the notion of causality and locality are considered. This allows us to compare the expressive power of different models within the same environment. In this respect, we have verified many of the examples given in the literature using our tool.