Abstract

Nowadays, when we model complex and real-time systems is very important to pay attention not only to the behaviour of the system, but also to the fact that the system must respect some properties, like reliability and safety. This kind of properties can be verified with a Petri Net, but building a complex system using it is very difficult, because the complexity of the resulting model can explode. Hence we want to build a system in an "easy" way watching at his behaviour, using Statecharts, and then we want to convert it "automatically" in a model that is much more effective in the analysis of properties, like Petri Net. For this purpose this paper will give an explanation of how to express Statecharts by means of Timed Petri Nets. Based on the semantic of these two formalisms we will show how to make the transformation using a step by step approach, with examples.

  Reading

• Report
• Presentation

  Abstract

Nowadays, when we model complex and real-time systems is very important to pay attention not only on the system behaviour, but also to the fact that the system must respect some properties, like for example, reliability and safety. This kind of properties can be verified with a Petri Net, but building a complex system using it is very difficult, because the complexity of the resulting model can explode. Hence we want to build a system in an ”easy” way watching at his behaviour, using Statecharts, and then we want to convert it ”automatically” in a model that is much more effective in analysis of properties, like Petri Net. For this purpose this paper will give an explanation of how to express Statecharts by means of Timed Petri Nets. We will show how to make the transformation using a rule based approach implemented in AToMPM and then we will discuss on the correctness and the limitations of the transformation.
Keywords: Model Transformation, Statechart, Timed Petri Net, TINA toolbox, AToMPM

  Implementation

• Report
• Presentation
• Project Material