General description
Related papers
Web interface
Some examples
Downloads
CSP2PN is a tool that automatically builds a Petri net [1, 5, 6] which produces
the same sequences of observable events that a given CSP specification [2, 7]. In CSP terminology, these sequences are the so-called traces (see, e.g., chapter 8.2 of
[7]). In Petri nets they correspond to transition firing sequences (see, e.g., [1]). The transformation algorithm uses
an instrumentation of the standard CSP's operational semantics as defined by A.W. Roscoe [7] to explore
all posible computations of a specification. The semantics is deterministic
because the rule applied in every step is predetermined by the initial
configuration. Therefore, the algorithm can execute the semantics several
times to iteratively explore all computations and hence, generate the
whole Petri net.
This semantics is an interesting result because it explicitly relates the CSP model
with the Petri net. The way in which the semantics has been instrumented can be used for other similar purposes with
slight modifications. For instance, the same design could be used to generate other
graph representations of a computation [3, 4].
This is the first approach that generates the Petri net as a side-effect of an
instrumented semantics.
The main advantage of this new approach is that the Petri net generated is
very similar (structurally) to the CSP specification. Every evaluation step of the semantics produces the associated (sub) Petri net.
CSP2PN is able to automatically generate a Petri net equivalent to a CSP specification. However, in the implementation the algorithm is much more complex because it contains some improvements that significantly speed up the Petri net construction. The most important improvement is to avoid repeated computations. This is done by:
MAIN = ASTRONAUT [|{|success|}|] NASA ASTRONAUT = mission -> MISSION MISSION = (fail -> STOP) [] (success -> STOP) NASA = success -> medal -> STOP |
It represents an astronaut that gets a medal from NASA if she succeeds in a space mission. Due to the choice operator, this specification can produce two different sequences of events, namely < mission fail > and < mission success medal > . Clearly, the same sequences are produced by the Petri net generated by the algorithm, as we can see in the next figure. In order to generate the Petri net, the algorithm performs two iterations; the first iteration generates the white nodes and grey nodes are generated in the second one.
[1] M. Hack. Petri Net Languages. Technical Report 159, Massachusetts Institute of Technology, Cambridge, MA, USA, 1976.
[2] C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
[3] M. Leuschel, M. Llorens, J. Oliver, J. Silva, and S. Tamarit. The MEB and CEB static analysis for CSP specifications. In Post-proceedings of the 18th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'08), Revised Selected Papers, LNCS 5438, Springer-Verlag, pp. 103-118, 2009.
[4] M. Llorens, J. Oliver, J. Silva, and S. Tamarit. An Algorithm to Generate the Contextsensitive Synchronized Control Flow Graph. To appear in Proc. of the 25th ACM Symposium on Applied Computing (SAC 2010), Sierre, Switzerland, 2010.
[5] T. Murata. Petri Nets: Properties, Analysis and Applications. In Proc. of the IEEE, vol. 77(4), pp. 541-580, IEEE Computer Society, 1989.
[6] J. L. Peterson. Petri Net Theory and the Modeling of Systems. Prentice-Hall, 1981.
[7] A.W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 2005.
This work has been partially supported by
The tool also provides a web interface that allows to test it online.
Astronaut1mission.csp -- In this specification there are two processes (ASTRONAUT and NASA) executed in parallel and synchronized on event {|success|}. It represents an ASTRONAUT that gets a medal from NASA if she succeeds in a space MISSION.
Astronaut2missions.csp -- In this specification there are two processes (ASTRONAUT and NASA) executed in parallel and synchronized on event {|success|}. Process ASTRONAUT represents an astronaut that participates in two missions after she graduates. Process NASA represents the NASA who gives her a medal when she concludes succesfully a mission.
Buses.csp -- This example describes a bus service with two buses running in parallel.
Prize.csp -- In this specification there are three processes (STUDENT, PARENT and COLLEGE) executed in parallel and synchronized on common events. Process STUDENT represents the three-year academic courses of a student; process PARENT represents the parent of the student who gives her a present when she passes a course; and process COLLEGE represents the college who gives a prize to those students which finish without any fail.
TrafficLights.csp -- This specification defines one car driving on one street. The street has one traffic light for cars controlling.
TrafficLights2.csp -- This specification defines one car driving on two streets. The car can circulate in two streets. Each street has one traffic light for cars controlling.
CSP2PN version 2.0 |
Linux version Mac OS X version |
CSP2PN version 1.0 |
Linux version Mac OS X version |
The verbose option -v is optional and can be activated to see a log of the transformation process.
|
Last update: 18/02/2010 18:09:12 |