Computational & Technology Resources
an online resource for computational,
engineering & technology publications
PROCEEDINGS OF THE SEVENTH INTERNATIONAL CONFERENCE ON ENGINEERING COMPUTATIONAL TECHNOLOGY
Transforming Communicating Sequential Processes to Petri Nets
M. Llorens, J. Oliver, J. Silva and S. Tamarit
Department of Information Systems and Computation, Universidad Politécnica de Valencia, Spain
M. Llorens, J. Oliver, J. Silva, S. Tamarit, "Transforming Communicating Sequential Processes to Petri Nets", in , (Editors), "Proceedings of the Seventh International Conference on Engineering Computational Technology", Civil-Comp Press, Stirlingshire, UK, Paper 26, 2010. doi:10.4203/ccp.94.26
Keywords: concurrent programming, communicating sequential processes, Petri nets, semantics, traces, implementation.
Communicating sequential processes (CSP) and Petri nets are two of the most important formalisms used to specify, model, verify and simulate complex concurrent systems. While CSP is a textual language, the formalism of Petri nets can be seen as a graphical tool. Therefore, both CSP and Petri nets try to solve the same problem from a different perspective, and thus each of them has its own advantages and drawbacks. Surprisingly, a transformation that enables a CSP specification to be converted into an equivalent Petri net does not exists (i.e., the language of events produced is exactly the same). Some partial solutions are [1,2,3,4]. This transformation would be very useful, from both a practical and theoretical perspectives. In particular, a transformation from CSP to Petri nets would allow us to graphically simulate a CSP specification; and it would also allow us to use the analyses and tools developed in the context of Petri nets with CSP specifications.
In this work we define an algorithm that transforms a CSP specification into an equivalent Petri net (i.e., it is not possible for an external observer to distinguish between them). The transformation is fully automatic, and hence, this result is very interesting because it allows CSP developers not only to graphically animate their specifications through the use of the equivalent Petri net, but it also allows them to use all the tools and analysis techniques developed for Petri nets.
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. In essence, our algorithm explores all possible CSP computations and incrementally generates a Petri net that models all the computations.
We have implemented the presented algorithm in a tool called CSP2PN. This tool allows us to automatically generate a Petri net equivalent to a given CSP specification. The implementation, source code and several examples are publicly available at: http://users.dsic.upv.es/~jsilva/CSP2PN/
purchase the full-text of this paper (price £20)