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 [5] 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/

1

F. de Cindio, G. de Michelis, L. Pomello, C. Simone, "A Petri Net Model of CSP", in "Proc. CIL'81", 392-406, Barcelona, 1981.

2

P. Degano, R. Gorrieri, S. Marchetti, "An Exercise in Concurrency: A CSP Process as a Condition/Event System", Advances in Petri Nets 1988, LNCS 340, Springer-Verlag, 185-105, 1988. doi:10.1007/3-540-50580-6_25

3

K.M. Kavi, F.T. Sheldon, S. Reed, "Specification and Analysis of Real-Time Systems using CSP and Petri Nets", International Journal of Software Engineering and Knowledge Engineering (IJSEKE), 6(2), 229-248, 1996. doi:10.1142/S0218194096000119

4

A. Mazzeo, N. Mazzocca, S. Russo, C. Savy, V. Vittorini, "Formal Specification of Concurrent Systems: A Structured Approach", The Computer Journal, 41(3), 145-162, 1998. doi:10.1093/comjnl/41.3.145

5

M. Llorens, J. Oliver, J. Silva, S. Tamarit, "Instrumenting the CSP Semantics to Generate a Petri Net", Technical report DSIC, Department of Information Systems and Computation, Universidad Politécnica de Valencia, Spain, February 2010. http://www.dsic.upv.es/~jsilva

purchase the full-text of this paper (price £20)

go to the previous paper
go to the next paper
return to the table of contents
return to the book description
purchase this book (price £125 +P&P)