DSL's Translational Semantics, Verification, Process Engineering, SimplePDL, Petri nets, Tina. |
Building blocsThis use case is introduced through a modeling language example on which we would like to express a set of properties that have to be verified on all possible models. Our DSL is a simple process description language: SimplePDL.
SimplePDL is an experimental language for specifying processes.
The SPEM standard (Software Process Engineering Metamodel) proposed by the OMG inspired our work,
but we also took ideas from the UMA metamodel (Unified Method Architecture) used in the EPF Eclipse plug-in
(Eclipse Process Framework), dedicated to process modeling. SimplePDL is simplified to keep the presentation simple.
The PetriNet metamodel is given in the figure 2. A Petri net (PetriNet) is composed of
nodes (Node) that denote places (Place) or transitions (Transition). Nodes are linked together by arcs (Arc).
Arcs can be normal ones or read-arcs (ArcKind).
The number attached to an arc specifies the number of tokens that are consumed in the source place or produced in the target one
(in case of a read-arc, it is only used to check whether the source place contains more tokens than the specified number).
Petri nets markings are defined by the tokensNb attributes of places.
Finally, we can express a time interval on transitions. A transition can only be started between min and maw time.
Tina (TIme Petri Net Analyser) is a software environment to edit and analyse Petri nets and temporal nets. The different tools constituting the environment can be used alone or together. Some of these tools will be used in this study:
The translation schema from a SimplePDL model into Petri netsThe translation schema that transforms a process model into a Petri nets model is given in the next figures. Each work definition is translated into four places characterising the state (NotStarted, Started, InProgress and Finished) in order to translate each WorkSequence by a read-arc between one source work definition place and the target work definition transition. We can remark that the state Started allows to memorise that one work definiton has already been started. We also add five places that will define a local clock. The clock will be in state TooEarly when the workdefinition ends before min_time and in the state TooLate when the work definition ends after max_time. The transformation is defined using three ATL rules (see the next listing). The first expresses one work definition in terms of places and transitions. The second translates a work sequence into a read-arc between the adequate place of the source work definition and the appropriate transition of the target work definition. The ATL resolveTemp operation is necessary because multiple places and transitions have been created for each WorkDefinition. Finally the last rule considers the whole process and builds the associated Petri net. We illustrate the SimplePDL2Petrinet transformation on simplified meta-models in order to keep the presentation simple. Other elements such as ressources, time and the fact that one activity can be split into multiple sub-activities have been modeled. The next figure shows the translation from one temporal WorkDefinition using resources. The next listing gives rules for consider Resource. In order to manipulate the obtained Petri net inside a dedicated tool such as Tina, we have composed the preceding transformation with a query PetriNet2Tina that translates the Petri net as a model of PetriNet into a textual form (.net) conforming to the concrete textual syntax of the Tina tool. Properties generation for process model validation
After expressing process models into Petri nets models, we want to check the properties associated to SimplePDL models using the Tina toolkit.
The main principle is to generate LTL properties using ATL queries.
We generate LTL formulas in textual form.
Therefore, we have to be aware of the translation shema from SimplePDL to PetriNet and Tina to ensure the consistency of the properties expression.
Working directly on PetriNet level would have require to formalize the LTL metamodel which seems to be irrelevant in such case.
Model consistency verification:
When the user elaborates his process model, he describes the constraints that will drive his process.
They can be causality relationships, like when a work definition is able to start only if some others are finished.
They can express the necessity to be able to use a certain amount of resources or even temporal constraints.
Once all such constraints are expressed, the user must be able to check whether his process is satisfiable. In other words, does one execution exists
that satisfies all causality constraints while respecting ressource usage and temporal restrictions?
Model-checking technics allows to reach this goal.
A process satisfying all such constraints is valid for us if it can terminates, i.e. it can reach a state where all its work definitions are in their finished state.
Other alternatives can be considered. This notion of termination must be defined at the SimplePDL level.
The macro-proposition
Transformation soundness:
Even if the translation is expressed in ATL at an adequate abstraction layer, it is still important to ensure transformation consistency. The resulting
Petri net model must be revelant with respect to the SimplePDL specification. But its complexity makes the analysis difficult.
To facilitate the definition of the ATL translation et to ensure the conformance of the resulting Petri net, we automatically
generate a set of LTL formulae which have to be satisfied by the Petri net translation of the initial SimplePDL process model.
These formulae are able to express that differents states modeled by a single value in the SimplePDL model have to be mutually exclusive in the Petri net one.
The following listing gives an example.
The set of these properties can be seen a |
None at the current time. |
[1] | Combemale, B, Garoche P-L, Crégut, X, Thirioux, X: Towards a Formal Verification of Process Model's Properties -- SimplePDL and TOCL Case Study. In: Proceedings of the 9th International Conference on Enterprise Information Systems (ICEIS), 12-16, June 2007, Funchal, Madeira - Portugal. |
[2] | (article in french) Combemale, B, Crégut, X, Berthomieu, B, and Vernadat, F: SimplePDL2Tina : Mise en oeuvre d'une Validation de Modèles de Processus. In: Proceedings of the 3ieme journées sur l'Ingénierie Dirigée par les Modèles (IDM), March 23th, Toulouse, France. 2007. |
[3] | (tutorial in french) Pantel, M, Crégut, X, and Combemale, B: La Méta-modélisation et la Transformation de Modèles (2007). |
Complete scenario |
Scenario SimplePDL to Tina available in the ATL transformation zoo (with source files). |
SimplePDL metamodel |
Full SimplePDL metamodel specified in KM3. |
PetriNet metamodel |
Full PetriNet metamodel specified in KM3. |
The present work is being supported by the Topcased project. |