Coloured Petri nets allow for modelling complex concurrent systems, but the specification of such systems remains a challenging task. Two approaches are generally used to lessen these difficulties: decomposition and refinement. Charles Lakos proposed three kinds of refinements for coloured Petri nets: type refinement, subnet refinement, and node (place or transition) refinement. This paper proposes new rules widening the scope of both type and transition refinements.
Coloured Petri nets are a specification language which presents the advantages of both a graphical description, giving an easy understanding of the model, and a formal semantics allowing for formal analysis techniques. However, as is the case for many specification languages, the specification of a system remains a difficult task. A way to alleviate these difficulties consists in using refinement techniques.
First, a rather simple model of the system is built, at a high level of abstraction, with few details. This abstract model constitutes a general description of the system. An incremental process of successive refinements is then applied, adding new details in a stepwise manner. The model is thus enhanced until all the expected behaviour and properties are taken into account. At each step, the abstract model is replaced by a refined one.
For defining refinements, the following questions should be addressed:
Since a model is characterised by its observed behaviour, the comparison between abstract and refined model will rely on it. Several notions of equivalence and order have been proposed in the literature. In particular, Lakos and
behaviour in R has a corresponding behaviour in A” (thus a refinement, while it may introduce further details, cannot introduce behaviours that would be new to the abstract model; this is useful to be able to explore the state space in a modular and still meaningful way). They express this relation between coloured Petri nets as a system morphism (behavioural morphism) from the refined model to the abstract one. Three kinds of refinements were proposed, and the system morphisms defined accordingly: type refinement, subnet refinement and node (place or transition) refinement. Transformation rules on the net structure, the colours and firing modes, that respect these morphisms, complete their work by providing practical refinement mechanisms.
This paper extends these coloured Petri nets refinements, and more
specifically the type and transition refinements. Type refinement includes two
constraints: the subtype relation defined by Liskov and Wing [
The paper is organised as follows. In Section 2 definitions of coloured Petri nets and system morphisms are recalled. Then, Section 3 recalls the refinements defined by Lakos and Section 4 the subtyping relation of Liskov and Wing. Our new refinement rules are then defined and proven correct in Sections 5 and 6. They are implemented in a tool for Petri net design, described in Section 7. 2
In this section, we recall the necessary definitions and notations from [
For a type universe Σ, we denote the set of functions from one type of Σ to another by ΦΣ = {X → Y | X, Y ∈ Σ} and by μX = {X → N} the set of multisets over a type X ∈ Σ.
where:
A coloured Petri net is a tuple N = hP, T, A, C, E, M, Y, M0i
2. T is a set of transitions such that P ∩ T = ∅; 3. A is a set of arcs such that A ⊆ P × T ∪ T × P ;
C : P ∪ T → Σ; 5. E is a function associating an expression with each arc: E : A → ΦΣ with
E(p, t), E(t, p) : C(t) → μC(p); 6. M is the set of markings: M = μ{(p, c) | p ∈ P, c ∈ C(p)}; 7. Y is the set of steps: Y = μ{(t, c) | t ∈ T, c ∈ C(t)} 8. M0 ∈ M is the initial marking.
For a node x ∈ P ∪ T , we denote by – •x the preset of x, i.e. •x = {y ∈ P ∪ T |(y, x) ∈ A}; – x• the postset of x, i.e. x• = {y ∈ P ∪ T |(x, y) ∈ A}.
In the following, E− denotes the expressions of arcs from places to transitions and E+ from transitions to places. The firing rule of a coloured Petri net is now defined.
Definition 2. Let N be a coloured Petri net. A step Y ∈ Y is firable from a marking M ∈ M, denoted M [Y i iff M ≥ E−(Y ).
In order to replace a node of a Petri net by a subnet during the refinement
process, the connections between these and their environment must be
considered. Therefore, we now define the border nodes on each side, adapted from [
System morphisms were defined in [
c c c c out1 offer 1 offer 2 c out2 ts1 ts2 1. φ is surjective on Pa, Ta, Aa; 2. φ is linear and total on the set of markings Mr and the set of steps Yr; 3. ∀Mr ∈ [M0ir, ∀Yr ∈ Yr: if Yr is complete, can be decomposed into Y1, Y2 ...
Yn, and is realisable from marking Mr, then φ(Yr) can be decomposed into φ(Y1), φ(Y2) ...φ(Yn), and is realisable from marking φ(Mr). 4. ∀Mr ∈ [M0ir, ∀Yr ∈ Yr : Yr is complete ⇒ φ(Mr + Er+(Yr) − Er−(Yr)) = φ(Mr) + φ(Er+)(φ(Yr)) − φ(Er−)(φ(Yr)).
In Definition 4, (3) indicates that when a step in Nr is decomposable, the corresponding step can be obtained by projection on Na, while (4) states that only the effect of a step can be projected as well.
Definition 5. Let φ : Nr → Na be a system morphism. A step Yr in Nr is said to be complete if ∀ta ∈ Ta : ∀tr ∈ bdr (Tr \ Ta) : Yr(tr) = φ(Yr)(ta) 3
Three types of coloured Petri nets refinements are defined by Lakos in [
Type refinement is used when it is necessary to detail further the description of the information carried by tokens, and the transitions’ firing modes. Refinement then consists in replacing an abstract token type by another one, more detailed, called the refined type. The net structure remains unchanged. The type modification addressed by Lakos is the addition of a component. 3.2
Subnet refinement consists in adding new elements (places, transitions and arcs) to the net.
[
Node refinement is used when the modeller wishes to give additional information about one of the net elements (place or transition) by expliciting it further. It can thus be a place refinement if details concern a place (superplace) or transition refinement if a transition is concerned (supertransition). Lakos defined canonical refinements for both of these cases.
In its canonical form, a place refinement replaces a place by a place-bordered subnet, whereas a transition refinement replaces a transition by a transitionbordered subnet. 4
A subtype relation was defined in [
Types are denoted by a triple hO, V, M i where O is a set of objects, V is a set of values, and M is a set of methods.
The type specification should contain the following information: – the description of the set of authorised values; – for each method, the description of (i) its signature (number and types of arguments, result type and exceptions list), (ii) its behaviour in terms of preand post-conditions.
B. Liskov and J. M. Wing distinguish three kinds of methods, constructors that return a new object of the type, observers that return values of other types, and mutators that modify object values.
They also identify two kinds of subtyping relations: – Extension subtype where the subtype extends the supertype by introducing new methods and adding new states (or values). – Constrained subtype where the subtype constrains the supertype with more details on the methods or on the supertype values. When the supertype specification keeps open several possibilities, subtyping may reduce or eliminate some of them.
Considering the two kinds of subtyping relations above, we consider here the following operations on types: – add a component to a record – fix a component value – add a method – modify a method.
These operations on types appear in the subtype relations as follows. 1. Extension Subtype The operations on types considered are the introduction of new methods and/or the addition of new states.
– New method introduction • if the method introduced is a constructor, it should take into account the invariant preservation; • if the method introduced is an observer, this has no consequence on the fact that the subtype preserves the supertype properties; • if the method introduced is a mutator, this may have consequences on the fact that the subtype should preserve the supertype properties. After a mutator is invoked, the new object value should belong to the set of authorized type values (according to invariants and historical properties). – Addition of new object states (or adding a new variable in records): this has no effect on properties preservation, and the abstraction function forgets the added variable. 2. Constrained Subtype The operations considered here are constraints on the object values and/or method modification with the aim to add more precision.
– Constraints on the object values (this may correspond to fixing a variable
value in a record). This may be achieved by defining the set of values for
the subtype objects as a subset of the supertype values and this preserves
the supertype properties.
– Method modification. This modification must comply with the
subtyping rules defined in [
Let us recall that if σ is a subtype of τ and mτ is the τ method corresponding to method mσ of σ : – arguments contravariance states that mτ and mσ should have the same number of arguments, and type αi of the ith argument in mτ should be a subtype of type βi of the corresponding argument in mσ. – either mτ and mσ return a result or do not return a result. If both methods return a result, the result covariance states that the type of the result returned by mσ should be a subtype of the type of the result returned by mτ .
An initial definition of type refinement was proposed by Lakos in [
Therefore, in this section, we extend the relation between the refined type
and the abstract type by considering the sub-typing relation defined by Liskov
and Wing in [
Data types modified [arc expressions or methods used in arc expressions modified]
Net behaviour may be changed ⇒ check LC
When performing type refinement, the net structure remains unchanged. Hence the only elements which may change the net behaviour are the values of arc expressions, and transitions guards.
Arc expressions Subsequently to a type refinement, an arc expression function might be modified. Figure 2 summarises the impact of type modification on arc expressions.
In the following, Er denotes arc expressions in the refined net, and corresponding arc expression in the abstract net.
Ea the Unchanged arc expressions If the arc expression is the same, i.e. Er = Ea, the following cases may occur: 1. adding a component to a tuple, setting the value of a component, adding a method, are changes that respect LC; 2. modification of a method leads to the following situations: – Ea does not refer to a method modified by the refinement. The values returned by Er and Ea are thus the same, and the net behaviour remains unchanged ; – Ea refers to methods changed by the refinement. Hence, although the expressions are the same, the values returned by Er and Ea may differ. Therefore the behaviour can be different as well, and we need to check that the effect of firing for each firing mode in the refined net is the same, once abstracted, as for the corresponding firing in the abstract net. Modified arc expressions When an arc expression is modified due to the refinement process, values of Er and Ea may differ, whatever the refinement operation. Hence, adding a component, setting the value of a component, adding a method may all modify the net behaviour. The expression modification should be performed so that it satisfies LC.
expression associated with a guard. However, two cases may occur (see Fig. 3): – the guard does not refer to a method modified by the type refinement: it has thus no influence on the transition behaviour; – the guard refers to methods modified by the type refinement. Hence the values returned by the refined and abstract guard expressions may differ. If the guard returns true in the refined net, it must also return true in the abstract net. 5.2
The net in Fig. 4(a) models a request for material issued from e.g. a service to the accountant. When material is needed, a request is issued. After the accountants check the request, they order the articles.
In a first approach to modelling the problem, the net describing the overall process can de considered. It uses a neutral colour, as shown in Fig. 4(a).
Then additional detail can be introduced, giving characteristics of the article to order, i.e. its number, its designation (name), its origin, the quantity required (qty) and the unitary price. The new type is thus obtained by adding components, as shown in the declarations below and Fig. 4(b). In this case, no arc or guard expression is changed, therefore LC is satisfied. It is also consistent with the subtyping conditions.
In order to take into account calls for offers when the price is above a certain level, a method is added which returns the total amount of the purchase Type modification [Type methods changed in guards]
Check that a guard returning true for a refined marking also returns true for the corresponding abstract marking x y z
Buy Buy x y z
DOT Delivered ARTICLE Delivered ARTICLE_1 Delivered price ∗qty (see type ART ICLE_1) in the declarations and Fig. 4(c)). This modification adds an observer method which returns a value, and is consistent with the subtyping relation. It is not used in arc or guard expressions, and therefore LC holds.
Declarations: DOT is a predefined neutral type Colset ARTICLE = record number:NAT * origin:STRING *
name:STRING * price:Rat * qty:Rat; Colset ARTICLE_1 = record number:NAT * origin:STRING * name:STRING * price:Rat * qty:Rat; fun amount = (#price ARTICLE_1 * #qty ARTICLE_1)::Rat; var x : DOT; var y : ARTICLE; var z : ARTICLE_1; var name : STRING; var price : Rat; var qty : Rat; 6
The canonical transition refinement proposed by Lakos, firing an abstract transition features firing a set of sequences of refined transitions, starting with transitions from the input border and ending with transitions from the output border of the refined part.
The underlying idea of the new refinement we propose here is to replace an abstract transition by a subnet containing alternative transitions plus internal places and transitions. Each of the alternative transitions is abstracted as the original abstract transition. This refinement aims at splitting a transition describing a general behaviour into several exclusive cases which then handle in more detail specific situations. For example, the net in Fig. 5(b) is a refinement of the one in Fig. 5(a): transition ta is replaced by a subnet Nta . To improve readability, ta has a single input place and a single output place (but this is not a constraint in the general case).
Definition 6. Let Nta = (Pta , Tta , Ata , Cta , Eta , Mta , Yta , Mta0 ) be a subnet. A morphism φ : Nr = (Pr, Tr, Ar, Cr, Er, Mr, Yr, Mr0)
→ Na = (Pa, Ta, Aa, Ca, Ea, Ma, Ya, Ma0) is a refinement with alternative transitions of ta ∈ Ta, where Nr is the refined net obtained by replacing abstract transition ta by Nta ) in the abstract net Na if: 1. ∀pr ∈ Pr \ Pta : ∀tr ∈ Tr \ Tta : φ(pr) = pr ∧ φ(tr) = tr ∧ (pr, tr) ∈ Ar ⇒ ((pr, tr) ∈ Aa ∧ Er(pr, tr) = Ea(pr, tr)) ∧ (tr, pr) ∈ Ar ⇒ ((tr, pr) ∈ Aa ∧ Er(tr, pr) = Ea(tr, pr)). Apart from transition ta the abstract net remains unchanged. 2. Tta = Talternative ∪ Tother The transitions replacing ta are of two kinds: the alternatives, and the others. 3. ∀t ∈ Talternative , •ta = •t \ Pta ∧ ∀p ∈ •ta : Ea(p, ta) = Er(p, t) All input places of ta are also input places of all alternative transitions, and are the only such abstract places. 4. ∀t ∈ Talternative , t•a = t• \ Pta ∧ ∀p ∈ t•a : Ea(ta, p) = Er(t, p)
All output places of ta are also output places of all alternative transitions, and are the only such abstract places. 5. ∀M ∈ Mr : ∀t0 ∈ Talternative : φ(M )[ta > ∧ M [t0 > ⇒ ∀t ∈ Talternative \ {t0}, ¬(M [ t >)
ing (so that the token flow is preserved). This can be ensured by guards or internal places of the Nta subnet.
E1
T
E2
pout (a) Abstract transition to be refined [guard1] talter1 taltern [guardn] pin 1
E E 1
E 2 2 E
pout (b) Refinement of transition ta 6. ∀t ∈ Talternative ∧ ∀c ∈ Cr(t) : φ(1 ‘(t, c)) = 1 ‘(ta, φ(c))
Firing an alternative transition has the same effect as firing ta. Firing a step in the refined net has the same effect as in the abstract net. 7. ∀p ∈ Pr : ∀c ∈ Cr(p) : φ(1 ‘(p, c)) = 1 ‘(p, c) if pr ∈ Pr \ Pta , φ(1 ‘(p, c)) = ∅ otherwise.
The internal marking of Nta is ignored by the refinement.
According to definition 6(1) φ is surjective over Pa, Ta, Aa. φ :Nr →
Na is a From (8), the abstract marking is obtained by ignoring the subnet marking. Hence, φ is linear and total over Mr.
From (6), the firing of an alternative transition corresponds to firing the abstract transition. Hence, φ is linear and total over Yr.
From (6) ∀Yr ∈ Yr, Yr is complete since only one of the alternative transitions can be fired in a given marking.
From (3), (4) and (7), ∀Yr ∈ Yr, ∀Mr ∈ Mr si Mr ≥ Er−(Yr) then φ(Mr) ≥ φ(Er−)(φ(Yr)) and φ(Mr + Er+(Yr) − Er−(Yr)) = φ(Mr) + φ(Er+)(φ(Yr)) − φ(Er−)(φ(Yr)). φ(Mr +Er+(Yr)−Er−(Yr)) is the effect after abstraction of the firing of the refined step Yr from the refined marking Mr and φ(Mr) + φ(Er+)(φ(Yr)) − φ(Er−)(φ(Yr)) the effect of the firing of the abstract step φ(Ya) from the abstract marking φ(Ma).
Let us consider again the example of Sect. 5.2, with the abstract net in Fig. 6(a). We now want to explicit the accounting rules: if the amount of the purchase is greater than some limit, a call for offers must be issued (see Fig. 6(b)).
Transition Buy has been replaced by two alternative transitions: Direct purchase et Ask offer.
We designed CPN Refiner so as to support the development of coloured Petri
nets following the approach proposed in [
Let us recall that the Petri net development method presented in [
CPN Refiner supports both the coloured Petri net development given the (typed) state observers and the events (together with their pre and postconditions), and its refinement. CPN Refiner supports node refinement and subnet refinement according to the principles stated in this paper. Type refinement is supported via a mere type modification.
Figure 7 shows the screen where the user entered the state observers and the events for a workshop example, and the generated Petri net is shown in Figure 8. A refined Petri net obtained through alternate transition refinement is shown in Figure 9.
CPN Refiner is build using Java Swing (Eclipse), API JDOM to handle the XML resulting file, library JGraph for the graphical presentation Petri nets. 8
Refinement is used to build a more detailed model (the refined model) from an abstract model. Several refinement notions have been proposed for different aims and various languages, and the work of Lakos deals with refinement for coloured Petri nets. An important point he states is that a model R is a refinement of a model A if for each behaviour of R there is a corresponding behaviour of A. More specifically, he defines three kinds of refinement, type refinement, node
Fig. 9. Workshop example: refined Petri net refinement (for places or transitions), and subnet refinement, so as to insure this behaviour correspondence.
In this paper, we extend the type refinement and the node refinement proposed by Lakos. For type refinement, we propose two constraints. The subtype relation as defined by Liskov and Wing that should exist between the refined and the abstract type, and Lakos’ refinement relation between the refined and the abstract model. We consider four operations on types, that are to add a component, to fix a component value, to add a method, and to modify a method. We studied the conditions that ensure that these operations guarantee both Liskov and Wing subtyping relation and Lakos refinement relation. We also extend the node refinement with a new rule for transitions refined by alternate transitions. This new rule complies with Lakos’ refinement principle.
A model development method was proposed for coloured Petri nets in [