Transforming Communicating Sequential Processes to Petri Nets

CSP and Petri nets are two of the most important formalisms used to specify, model, verify and simulate complex concurrent systems. Both models have been successfully used in the industry and there are many verification, simulation and analysis techniques for them. Surprisingly, there does not exist a transformation that allows to convert a CSP specification into an equivalent Petri net (i.e., the language of external events produced is exactly the same). In this paper we formally define a fully automatic transformation that translates a CSP specification into an equivalent Petri net. This is the first approach that generates the Petri net as a side-effect of an in-strumented semantics. Our transformation relies on the definition of an operational semantics for CSP that extends the standard semantics with the ability of producing a Petri net that simulates the execution performed by the semantics. This means that, given a computation with the extended semantics, it produces the same result as the standard semantics, but it also produces as a side-effect the Petri net associated to the performed computation. The main advantage of this new approach is that the Petri net generated is very similar (structurally) to the given CSP specification. Finally, the algorithm is implemented in a tool called CSP2PN