In order to show the application of our translation algorithm, we applied it to the CD player case study.

UML state machine of The CD player

In this picture the example of the CD player with two principal states: BUSY and NONPLAYING.
The player switches from the state NONPLAYING to BUSY (and vice versa) depending on which button the user presses. The player switches from state CLOSED to OPEN when the user presses the button (depicted by a transition labelled with load) and vice versa. The player changes from the state NONPLAYING to the state BUSY when the user presses the button play (depicted by a transition labelled with play). We can switch from the state PLAYING to the state PAUSED by pressing the button pause (depicted by a transition labelled with pause). The same button allows the change from the state LIGHTON and LIGHTOFF. If the user presses the button stop (depicted by a transition labelled with stop), the player reads all tracks in the CD (depicted by a transition with a guard on track) or the user presses the button load (depicted by a transition labelled with load), then the player switches from the state BUSY to the state NONPLYING (more precisely, switches to the state closed for the rst two cases and to the state open for the third on

Coloured Petri Net of the CD player

As showed, we present the translation of the CD player example. Each simple state is translated to place, each transition from a simple or composite state is translated to a CPN transition and so on. The CPN source of the CD player model is available here.


After the translation, we can do the verification on the system  by verifying some properties. In the picture, there is textual part where we put the formulation of properties, a binder that contains the different options that we can apply to the CPN and a green rectangle that contain the result after the evaluation the textual part.  In this example we verify the following properties:​
  1. the CD player cannot be both closed and open
  2. whenever the CD player is in state PLAYING, there is a CD in the player
  3. THe value of track never exceeds trackCount