BolitaAzul You can test CSP2PN online using the new web interface

C S P 2 P N :  T r a n s l a t i n g   C S P   t o   P e t r i   n e t s

Index:

Bolita General description
Bolita Related papers
Bolita Web interface
Bolita Some examples
Bolita Downloads


  G e n e r a l   D e s c r i p t i o n

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:

Example

Consider the following CSP specification:

    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.

SOC


 R e l a t e d   P a p e r s  a n d  P r o j e c t s

[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

 W e b   I n t e r f a c e

The tool also provides a web interface that allows to test it online.

S o m e   E x a m p l e s

bolita roja 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.

bolita roja 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.

bolita roja Buses.csp -- This example describes a bus service with two buses running in parallel.

bolita roja 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.

bolita roja TrafficLights.csp -- This specification defines one car driving on one street. The street has one traffic light for cars controlling.

bolita roja 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.

  D o w n l o a d s

CSP2PN version 2.0

Linux version

Mac OS X version
CSP2PN version 1.0

Linux version

Mac OS X version

 

Installation/Execution

  1. Download the zipped file above.
  2. Unzip the downloaded file in any folder (tar xvzf csp2pn_linux_x86-64.tar.gz).
  3. Run

    The verbose option -v is optional and can be activated to see a log of the transformation process.

  

MiST GPLIS DSIC UPV
Last update: 18/02/2010 18:09:12