Investigate the suitability of CPN Tools for model verification

[srieger]

SP: 34
CPN Tools is an open source tool suite supporting advanced modelling with coloured Petri nets and real-time aspects. CPN Tools offer graphical tools for modelling, simulation and formal verification.

CPN Tools seems to be a possible solution for model verification in general and timed verification in particular. As the timed automata tool UPPAAL is not open source it seems that CPN Tools may be a replacement. The modelling language should be strictly more powerful.

This task covers the following subitems:

• Analyse CPN Tools with respect to expressive power, modelling capabilities and property language
• Build a small example model from the ETCS domain
• deferred Comparison of UPPAAL and CPN Tools
• Investigation of Eclipse integration (there is already some facility) - cancelled
• deferred How can the transformation of SysML statecharts to the CPN Tools language be achieved?
• deferred How can the transformation of SysML activity diagrams to the CPN Tools language be achieved?
• Are CPN Tools suitable for test case generation and writing adaptor code for testing code to be executed on the simulator?
• deferred Using CPN visualisation capabilities to communicate verification results with non-experts.

@srieger
@janWelte
@christianstahl

[srieger]

We wish to change the title of the issue from
"Investigate the suitability of CPN Tools for timed verification (possible replacement for UPPAAL)"
into the more general
"Investigate the suitability of CPN Tools for model verification and test case generation"

Could someone please do this for us? Many thanks!

[janWelte]

As discussed in the telco today. I would lime to assist with this issue.

[srieger]

That's really great, Jan. I have just begun to have a look at CPN Tools.

[srieger]

I created a first version of a CPN "Start of Mission" model. See #88.

[janWelte]

I've check your model. An think it is a good first step (especially as it shows how Petri nets can be used) to model the specifications. Clearly there is a number of things which can be improved, but these are mainly related to the way the specifications are writen.
At the moment I'm laking a vision how to proceed with this specific model.

Shall I try to enhance the model by creating a more linear structure?
Shall we try to name certain timing constraints, which we then try to check on the model?

Do you have a suggestion?

[srieger]

Thank you for your help, Jan.

Do you think we can specify timing constraints? In the specification there is no mentioning of them. Of course, for example regarding the setup of a radio session, some of the timings can be obtained from other parts of the standard.

Do you think we will get traceability issues when linearising/optimising the Petri net? We could certainly remove the concrete data that is currently in there and just consider the state of the individual data items. This would already simplify the structure a bit.

[MarcBehrens]

@srieger there are some timing restrictions mentioned in Subset-026-A3 which also have a timing influence within the Start of Mission:
e.g.:

• MA request repetition cycle, default value 60 s TCYCRQSTD
• Maximum time to maintain a communication session in case of failed re-connection attempts 5 minutes
• Max. time for train trip suppression when override function is triggered 60 s T_NVOVTRP
• The number of times to try to establish a safe radio connection. 3 times
• Repetition of radio messages (i.e. excluding the first sending) 3 times
• Waiting time before radio message repetition 15 s

[srieger]

Dear @MarcBehrens,

thanks for your input. We have not incorporated timing yet, but this might be interesting. All of these things are however "external" to Start of Mission but of course they influence the timing there.

[MarcBehrens]

subtask

• Comparison of UPPAAL and CPN Tools
  will be extended to the
• transformation between CPN Tools and model checker
• Tina is a candidate @dalzilio

e.g. what happens if a message is delayed applied to SRS chapter 5 - procedures with the aim to have a complete view on all the procedures