Modular extensions of Petri Nets: a survey - Software Modeling and ...

Alexis Marechal Université de Genève, Centre Universitaire d’Informatique 7 route de Drize, 1227 Carouge, Suisse

Didier Buchs Université de Genève, Centre Universitaire d’Informatique 7 route de Drize, 1227 Carouge, Suisse

Technical report #218 (Friday 22nd June, 2012)

Modular extensions of Petri Nets: a survey

Software Modeling and Verification Department of Computer Science University of Geneva Battelle Bat. A Route de Drize 7 CH-1227 Carouge Switzerland

Abstract Modularity in Petri nets is an important topic that has been studied for years. It is a mandatory principle for using Petri Nets in real size systems and also to promote reuse. Indeed, the introduction of high level nets solves the question of modeling multiple similar behaviors. However, modularity principles are needed to handle the heterogeneity of the concepts to model by using a divide and conquer approach. Although important to study, modular principles have been difficult to settle in the Petri net domain. A naive approach is to consider a syntactic approach, where modules have to be composed to create a single Petri net to compute the behavior. The prevailing approach is a semantic approach, where each module has its own semantics defined prior to composition. There exists a large variety of composition mechanisms such as place fusions, transition fusions and synchronization mechanisms. Synchronization mechanisms are the more elaborated way of linking modules. They may be asynchronous or synchronous and may impose transactional or atomicity principles. An additional dimension is present in the object-oriented approach, when modules are dynamically created and referenced. This document is an attempt to make a state of the art in the domain of modularity for Petri nets. The main objective is to stress out the vast array of modular mechanisms that have been defined over the years instead of exploring all the existing modular formalisms. Keywords: Petri Nets, Modularity, Composition, Object-oriented

Contents 1 Introduction

1

2 Classification of the modular formalisms 2.1 List of formalisms . . . . . . . . . . . . . . . . . . . . . 2.2 Synopsis . . . . . . . . . . . . . . . . . . . . . . . . . . 2.3 P/T Petri net (P/T) or High Level Petri net (HLPN) 2.4 Module structure . . . . . . . . . . . . . . . . . . . . . 2.4.1 Interface syntax . . . . . . . . . . . . . . . . . 2.4.2 Hierarchy . . . . . . . . . . . . . . . . . . . . . 2.4.3 Encapsulation of data types . . . . . . . . . . . 2.5 Communication/composition . . . . . . . . . . . . . . 2.5.1 Synchronous or asynchronous communication . 2.5.2 Duplication of service calls . . . . . . . . . . . 2.5.3 Non-deterministic/parametric communication . 2.5.4 Priorities . . . . . . . . . . . . . . . . . . . . . 2.6 Static and Dynamic instantiation . . . . . . . . . . . . 2.7 Inheritance and subtyping . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

1 1 2 4 4 4 5 5 5 5 6 6 7 7 8

3 Decription of the modular formalisms 3.1 Modular PT and CP-nets . . . . . . . . . . . . . . 3.2 Net components . . . . . . . . . . . . . . . . . . . . 3.3 Reentrant nets . . . . . . . . . . . . . . . . . . . . 3.4 Colored puzzle nets . . . . . . . . . . . . . . . . . . 3.5 Hierarchical CP-nets . . . . . . . . . . . . . . . . . 3.5.1 Substitution places and transitions . . . . . 3.5.2 Invocation transitions . . . . . . . . . . . . 3.5.3 Fusion sets . . . . . . . . . . . . . . . . . . 3.6 Place/Transition refinements . . . . . . . . . . . . 3.7 CP-nets with channels . . . . . . . . . . . . . . . . 3.8 Composition of nets based on CSP semantics . . . 3.9 Hierarchical High Level Petri nets . . . . . . . . . 3.10 Modular PNML . . . . . . . . . . . . . . . . . . . . 3.11 BIP . . . . . . . . . . . . . . . . . . . . . . . . . . 3.12 M-nets . . . . . . . . . . . . . . . . . . . . . . . . . 3.13 Communicative objects and cooperative nets . . . 3.13.1 Communicative objects . . . . . . . . . . . 3.13.2 Cooperative nets . . . . . . . . . . . . . . . 3.14 Object colored Petri nets (OCP-Nets) . . . . . . . 3.15 Object Petri nets . . . . . . . . . . . . . . . . . . . 3.16 Concurrent Object-Oriented Petri Nets (CO-OPN) 3.16.1 A general component-oriented formalism . . 3.16.2 CO-OPN . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . .

9 9 11 11 12 13 13 16 18 19 20 21 22 23 25 25 27 27 28 28 29 31 31 33

4 Conclusion

. . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . .

34

1. INTRODUCTION

1

1/34

Introduction

Petri nets are a well known formalism used to model concurrent discrete systems in a compact way, and perform verification on them. As models grew larger, High Level Petri nets (HLPNs) have been proposed. In HLPNs, data is carried by tokens and manipulated by operations attached to output arcs of transitions. This solved the problem of modeling systems with identical components. However, the use of such high-level models proves not to be sufficient. When modeling a large system, the modeler often decomposes its model into different parts with clearly identified separate functionalities. This natural decomposition can also be used in the formal model to simplify the modeling and verification activities. Here we consider modularity as the existence of separate entities in a model, along with the description of composition mechanisms. We distinguish the notions of syntactical composition, where the modules are first combined into a complete model before computing the semantics, and semantical composition where there is a definition of the semantics of the composition based on the semantics of each module. In [ZHLR95], these two notions have been called respectively composition and modularity. There are many different modular formalisms presented as extensions of Petri nets, either for low-level P/T Petri nets (P/Ts) or HLPNs, with different objectives in mind. Some formalisms are meant to simplify the modeling activity by allowing the user to create simple nets and compose them later. Some others were defined to simplify the verification process, by abstracting irrelevant behaviors. Finally, some formalisms aim to raise the expressivity of Petri nets, in order to create models closer to the actual systems. Of course, most formalisms combine different of these objectives. In this report we will have a quick glance at some modular formalisms that were proposed in the literature. Making a full state of the art is not in the scope of this document, as this would be a nearly impossible task, given the high number of formalisms that were proposed (and are still proposed) over the years in the Petri nets community. Moreover, for clarity and brevity reasons, we will only make a superficial description of each formalism rather than going into detail in the formal definitions. This document is organized as follows: in Section 2 we give some possible classification criteria for the modular Petri nets-based formalisms we selected for this document. A quick description of each of these formalisms are to be found in Section 3. Section 4 concludes the survey.

2

Classification of the modular formalisms

This document describes some different formalisms, which constitute a small part of the whole state of the art in the domain of modularity in Petri nets. These formalisms cover a wide range of different concepts, with very different objectives. In this section we give a classification of the most important characteristics found in this survey. We first mention the list of formalisms that we considered. Some explanations about each formalism are given in Section 3. Then we present a table describing the classification we established. Afterwards, we give a quick explanation of each characteristic found in this table.

2.1

List of formalisms

Here we present a list of the formalisms that were described in Section 3, as a reference for the rest of this section: • Modular CP and PT-nets (Section 3.1);

2. CLASSIFICATION OF THE MODULAR FORMALISMS

• Net components (Section 3.2); • Reentrant nets (Section 3.3); • Colored puzzle nets (Section 3.4); • Hierarchical CP-nets (Section 3.5); • Place/Transition refinements (Section 3.6); • CP-nets with channels (Section 3.7); • Composition based on CSP semantics (Section 3.8); • Hierarchical High Level Petri nets - HHPN (Section 3.9); • Modular PNML (Section 3.10), • Behavior, Interaction, Priority - BIP (Section 3.11); • M-nets (Section 3.12); • Communicative objects and cooperative nets (Section 3.13); • Object Colored Petri nets - OCP-Nets (Section 3.14); • Object Petri nets (Section 3.15); • CO-OPN (Section 3.16);

2.2

Synopsis

Table 1 show a synopsis of all the classification criteria presented in this section.

2/34

none labels labels labels other labels other labels labels labels labels other other

" " " " " "

"

" " "

" " " " "

" " " " " "

"

"

Inheritance & Subtyping **

Priorities

Parametric communication

Non-deterministic communication

Duplication of service calls *

Variable sharing

Asynchronous messages

Synchronous communication

" " " " " " " " "

" " " "

Dynamic instantiation

Modular CP-nets Colored puzzle nets Hierarchical CP-nets CP-nets with channels HHPN Modular PNML BIP M-nets Communicative objects Cooperative nets OCP-nets Object Petri nets CO-OPN

"

"

Instantiation

Static instantiation

none labels labels none labels

Encapsulation of data types

Hierarchy

Interface P/T HLPN

Modular P/T nets Net components Reentrant nets P/T refinements CSP comp.

Communication

" " " " " " "

" " " " " " "

" " " " " "

"

" " " "

" " " " "


Module structure

" " "

* Only for formalisms that define synchronous communication ** Only for formalisms that define static of dynamic instantiation

Table 1: Summary of the characteristics of the modular formalisms 3/34


2.3

4/34

P/T or HLPN

We distinguish here the formalisms that work over P/Ts from those that work over HLPNs. P/T Modular PT-nets, net components, reentrant nets, place/transition refinements and composition based on CSP semantics. HLPN Modular CP-nets, colored puzzle nets, hierarchical CP-nets, CP-nets with channels, HHPN, Modular PNML, BIP, M-nets, communicative objects, cooperative nets, OCPNets, object Petri nets and CO-OPN. Note that we included BIP among the HLPN formalisms, even though the formal definition from [BSS09] was made on P/Ts. Indeed, BIP components have a set of internal variables, and the transitions firing modify the value of these variables. This could be represented using places in HLPN Petri nets. We see that there are a lot of formalisms that model modularity for HLPNs. Among the formalisms that are defined for P/Ts, most of them are special cases of fusion of places and transitions, which have already been generalized to Colored Petri nets (CPNs) by modular CPnets and hierarchical CP-nets.

2.4 2.4.1

Module structure Interface syntax

In most modular formalisms, there is a principle of encapsulation: some elements are accessible from the environment of the modules, and some other are internal to the modules. This helps the modelers to define models where modules are loosely coupled among them. We distinguish here three kinds of interfaces. First, in some formalisms, there is no interface declaration at all, and all objects are visible from the environment. Second, in some Petri net-based formalisms, some places or transitions are declared as belonging to an interface, making a distinction between interface places and transitions and internal places and transitions. A label associated to the places and transitions may indicate which ones belong to the interface and which ones are internal. Finally, some formalisms introduce new elements that do not belong to the standard definition of Petri nets to play the role of the interface. In this case we consider only the formalisms in which labels on places and transitions would not be enough to represent the interface. No interface declaration Modular PT and CP-nets and place/transition refinements. Interface is a set of labels applied to standard Petri nets elements Net components, Reentrant nets, Colored puzzle nets, Hierarchical CP-nets, CP-nets with channels, the composition based on CSP semantics, Modular PNML, M-nets, Communicative objects, Cooperative nets and OCP-Nets. Note that Modular PNML also defines modularity for the data types, not taken into account in this classification. Completely new elements added to the Petri nets syntax to form the interface : HHPN, BIP, Object Petri nets and CO-OPN. We see immediately that the majority of modular formalisms use simple labels (or some equivalent mechanism) on places and transitions to denote the interface of modules. Nevertheless, the most complex formalisms need to add new elements to the standard definition of Petri nets in order to express more powerful synchronizations.


2.4.2

5/34

Hierarchy

In some formalisms there is an explicit hierarchical relation between the modules: some modules are said to contain other modules, called submodules. In HHPN (see Figure 18) we see a clear example of this, as the hierarchy in HHPN is defined separately from the modules definitions. On the other hand, the two modules depicted in Figure 3 clearly have no hierarchical relation. Hierarchical definitions of the modules allows to define encapsulation of the modules themselves. Note that the definition of the notion hierarchy we use is very specific, other different definitions are often encountered in the literature. Hierarchy among components Hierarchical CP-nets, place/transition refinements, HHPN, Modular PNML, object Petri nets and CO-OPN. Note that Communicative objects and Cooperative nets are the only object-oriented formalisms that do not include a hierarchical definition. We can see that most formalisms do not have a hierarchical organization for modules, even though it is a standard mechanism. 2.4.3

Encapsulation of data types

As seen previously, most Petri nets-based modular formalisms define an interface, which allows a distinction between what element of a module are accessible from the environment, and what elements are encapsulated. Strangely, there are very few HLPN formalisms where the definition of the data types is itself encapsulated. Indeed, most of them define a monolithic structure for the data types, and every module can access all the values and functions of all data types. There is only one formalism in this survey that defines an encapsulation and composition of the data types: Modular PNML. This achieved by defining some values and operations as part of the module interfaces, and composing the data types by means of signature homomorphisms. Encapsulation of data types Modular PNML.

2.5 2.5.1

Communication/composition Synchronous or asynchronous communication

We consider here two principal kinds of communication, synchronous and asynchronous. Note that the distinction between both is not always clear. In general, we consider a fusion of transitions as a synchronous communication, and a fusion of places as an asynchronous communication. We divide asynchronous communication into variable sharing (where the modules have simultaneous read and write access to a single variable, e.g., with a fusion of places) and asynchronous message passing (where a module sends a message to another module and relinquishes the access to the message sent, e.g., when tokens sent from a module to an interface place of another module). Some languages define constructions for both synchronous and asynchronous communication styles. Synchronous communication Modular CP and PT-nets, place/transition refinements, composition based on CSP semantics, Hierarchical CP-nets, CP-nets with channels, HHPN, Modular PNML, BIP, M-nets, OCP-Nets, Object Petri nets and CO-OPN. Asynchronous message passing Hierarchical CP-nets, HHPN, communicative objects and cooperative nets and Object Petri nets.


6/34

Variable sharing Modular CP and PT-nets, Net components, reentrant nets, place/transition refinements, colored puzzle nets, Hierarchical CP-nets, Modular PNML, M-nets and OCPNets The only formalism that allows both place fusion and asynchronous message passing is the Hierarchical CP-nets. Indeed, in Hierarchical CP-nets, there is a place fusion, but there is a distinction between input places and output places. True variable sharing can be modeled in hierarchical CP-nets by labeling a place port as input and output at the same time. Both synchronous and asynchronous communications seem to be equally used in the literature. Note that asynchronous communication may be simulated by synchronous models, while the opposite is more complicated. 2.5.2

Duplication of service calls

An important application of Petri nets is the modeling of programming languages. To model the ubiquitous remote procedure call paradigm, one may use asynchronous message passing, or synchronous communication. In Petri nets, synchronous communication is usually modeled with some kind of transition fusion. When modeling the remote procedure call paradigm, using a simple fusion of transitions may be a problem: if two modules wish to call a procedure of a third module, and the call is modeled with transition fusions, both calls may be unwillingly synchronized. Some formalisms take this problem into account by specifying a special kind of asymmetric transition fusion. Whenever a module calls a function of another module, the corresponding transitions in the second module is duplicated before the fusion. This was explained in more detail for the special case of the Hierarchical CP-nets (see Figures 8 and 9). Note that this characteristic only makes sense for formalisms that define some kind of synchronous communication. Asynchronous communication trivially cannot cause an unwanted synchronization between procedure calls. No duplication of service calls Modular CP and PT-nets, place/transition refinements, HHPN, Modular PNML, BIP. Duplication of service calls Composition based on CSP semantics, Hierarchical CP-nets, CP-nets with channels, M-nets, OCP-nets, Object Petri nets, CO-OPN. 2.5.3

Non-deterministic/parametric communication

In most modular formalisms, the communications are defined between a fixed set of participants. This is not always the case, and some formalisms define a special kind of communication: non-deterministic and parametric communication. In this framework, the entities involved in a composition are not determined prior to runtime. They are rather determined during the computation of the semantics. Non-deterministic communication means that each time that a communication takes place, the entities involved are chosen non-deterministically between a given set of candidates. This choice may vary at each occurrence of the same communication. The perfect example of this kind of non-deterministic communications is the CP-nets with channels (see Figures 14 and 15). Parametric communications are quite similar. As in non-deterministic communications, the entities involved in a parametric communication are not pre-determined, but they are chosen at runtime. Nevertheless, they are not chosen non-deterministically, instead they are determined by a factor computed during runtime. A good example such communications are the M-nets (see Figure 23).


7/34

Non-deterministic communication CP-nets with channels, M-nets, Communicative Objects, Cooperative nets, OCP-nets, Object Petri nets, CO-OPN. Parametric communication M-nets, Communicative Objects, Cooperative nets, OCP-nets, Object Petri nets, CO-OPN. We can see that all the formalisms that support parametric communication also support non-deterministic communication, even though this is not mandatory. 2.5.4

Priorities

Priorities are a simple and relatively standard mechanism in Petri nets. A priority is an irreflexive asymmetric transitive relation between the transitions of a Petri net that add a supplementary condition to the firing of transitions: a transition can only be fired if no transition with higher priority can be fired. The same mechanism can be adapted for modular extensions for Petri nets, by creating a priority relation between the services offered and stating that a service can only be called if no service with a higher priority can be called. The only formalism in this survey to implement this mechanism is BIP. Priorities definition BIP.

2.6

Static and Dynamic instantiation

A common feature of modular systems is the presence of more than one identical or very similar module. Thus, having instantiation mechanisms clearly facilitates the modeling and verification processes. Static instantiation is a very simple process, where a set of modules are defined to be identical or similar to a template. Few formalisms give an explicit static instantiation mechanism, even if almost all of them could implement one without difficulty. On the other hand, some formalisms allow dynamic instantiation, that is, the creation (and usually destruction) of modules during the execution of the net. Contrary to the static instantiation, this clearly has an important impact in the semantics of the formalisms. Explicit static instantiation Hierarchical CP-nets, Modular PNML, OCP-nets, Object Petri nets and CO-OPN. Dynamic instantiation Hierarchical CP-nets, Communicative objects, Cooperative nets, OCP-Nets, Object Petri nets and CO-OPN. Static instantiation of modules is not usually described even if it is a very simple and important process. Its simplicity is probably the main reason for not defining it. Most of the formalisms that define a static instantiation mechanism also define dynamic instantiation. Most of them use the nets within nets paradigm, where some tokens in the Petri net places are references to other Petri net modules. Hierarchical CP-nets are the exception to this, as they allow dynamic instantiation by means of invocation transitions instead of nets within nets (see Section 3.5.2). Note that we did not include the Communicative objects and Cooperative nets as formalisms that define static instantiation, even though they define dynamic instantiation. Indeed, the other nets within nets formalisms in this survey (OCP-nets, Object Petri nets and CO-OPN) define explicitly a static instantiation mechanism, separated from the nets within nets. Thus, we wanted to separate the two instantiations and point out the fact that some formalisms have a separate mechanism for both of them.


2.7

8/34

Inheritance and subtyping

Formalisms that define static and/or dynamic instantiation have the notion of types of Petri nets. The template used to instantiate defines a type, and all the instances of that template are said to be of the same type. Inheritance and subtyping are two distinct relations between the types. Inheritance is a syntactic mechanism to create types based on previously defined types. If a type inherits from a second type, it copies the features of the latter and eventually adds some more. Subtyping is a different relation between types. It implies a semantic substitutability principle: an instance of a type may always be replaced by an instance of its supertype, without changing the semantics of the whole system. Even though these two notions are distinct, the three formalisms that define one of them also happen to define the other. We did not find a formalism that explicitly defines an inheritance relation without also defining a subtyping relation, even though one is not necessarily related to the other. Indeed, any formalism that defines an interface may easily define an inheritance relation, but a subtyping relation is usually more complex to define. Inheritance and subtyping OCP-nets, the Object Petri nets and CO-OPN.

3. DECRIPTION OF THE MODULAR FORMALISMS

3

9/34

Decription of the modular formalisms

This section gives a quick informal description of the modular extensions of Petri nets considered in this document. Rather than making a full state of the art, the objective is to illustrate the important heterogeneity in the methods used by the Petri nets community to model modular systems. Instead of making a full study of the syntax and semantics of the formalisms, we describe each one of them mainly by using small examples. Most of this examples were directly taken from the papers in which the respective formalisms were published. Some of the formalisms presented have very complex semantics definitions. Because of this, we limit our description to the sole description of the modular mechanisms, leaving out all the other concepts.

3.1

Modular PT and CP-nets

In [CP00], Christensen and Petrucci described the perhaps most well known mechanism for modularity in P/Ts: fusion of places and transitions. This was later extended for CPNs in [CP92], leading to a formalism called modular CP-nets. In this work, a modular (CP-)net is a set of modules, that are standard (colored) Petri nets. Composition is declared by means of sets of places and transitions to be merged, called fusion sets. The result of the composition is a single (Colored) Petri net. For each place fusion set (resp. transition fusion set), there is a single place (resp. transition) in the resulting net. The incoming and outgoing arcs are the union of the arcs from the elements in each module. Any place and transition may be merged (with some restrictions on the domains of the places in the case of CPNs), thus there is not a clear definition of an interface (see Section 2.4.1). Note that when two transitions from the same fusion set have a variable in common in their input arcs, the variable is unified: both transitions are forced to take the same value from the corresponding place. Thus, the creation of a fusion set is dependent on the syntactic definition of each component. This breaks the encapsulation principle, as a result of the absence of an interface. Figure 1 shows an example of a modular CP-net, illustrating the fusion of transitions. The result of the fusion is shown in Figure 2. Fusion of places works in a very similar way to fusion of transitions. Declared interface None. Any place and transition can belong to a fusion set. Composition declaration The composition is declared by means of fusion sets. A fusion set is a set of places (resp. transitions) that are merged during the composition.


Figure 1: Example of modular CP-net from [CP92]

Figure 2: Result of the merge of the nets in Figure 1

10/34


3.2

11/34

Net components

In [Val94], Valmari proposed a formalism called net components, for P/Ts. It is very similar to the fusion of places in modular CP-nets. One difference is that a net component explicitly declares a set of border places, that have no initial marking. Only border places can be merged, all other places are internal to the component. There is an additional mechanism to "internalize" border places, which gives them an initial marking while removing them from the set of border places. Note that this formalism does not define transition fusion mechanisms. Thus, all communications are asynchronous. Figure 3 shows an example of the composition of two net components. Declared interface Some places are declared as border places, they do not have an initial marking. Composition declaration Fusion sets over border places.

Figure 3: Example of the composition of two net components taken from [Val94]

3.3

Reentrant nets

Chehaibar presented in [Che91] another formalism similar to fusion of places for P/Ts, called reentrant nets. The interface definition is a bit different, there is a set of initial and final places. There are two composition operators: choice and sequential. Both have special restrictions on the type of places that can be merged. The merging mechanism is otherwise similar to the previous formalisms. Figure 4 shows and example of the composition of two reentrant nets. Declared interface Some places are declared as initial and final places. Composition declaration Two composition operators are declared, to merge initial and final places of the components. The mechanism is similar to place fusion sets, with specific constraints for the two operators.


12/34

Figure 4: Example of the composition of two reentrant nets taken from [Che91]

3.4

Colored puzzle nets

Recently, Chatain and Fabre proposed in [CF10] a formalism called colored puzzle nets. Again, it is a special case of places fusion, but unlike reentrant nets and net components, colored puzzle nets have been defined for CPNs. Note that the central point of this work is to consider unfoldings of the components, both structural unfoldings (called expansions in [CF10]) and McMillan unfoldings. Here we only describe the modular formalism itself, not the semantic considerations behind. A colored puzzle net has a set of interface places, some declared positive, some declared negative. Positive places can be merged to negative places, the result is a normal internal place. Identifying the places to be merged is done through a set of labels assigned to the places.


13/34

Figure 5: Example of two colored puzzle nets and their composition taken from [CF10] Declared interface Some places are declared as interface places, either positive or negative. While unfolding the components, the interface places are not unfolded until they are merged to form into internal places. Composition declaration Similar to place fusion sets. Here, the places to be merged are identified with the help of labels: two interface places are merged if they have the same label. A positive place can only be merged with a negative place that has the same label.

3.5

Hierarchical CP-nets

Hubert, Jensen and Saphiro presented in [HJS91] a set of different mechanisms to enrich CPNs with the notion of modularity. These mechanisms include the fusion of places and transitions that we have seen in the previous formalisms, and goes beyond, adding a notion of instantiation (static and dynamic) and page hierarchy. In the rest of this document we find a lot of mechanisms similar to those described here for hierarchical CP-nets. Thus, our description of this formalism is more detailed than any other. We will divide the different modular mechanisms in three: substitutions of transitions and places, invocation transitions and finally fusion sets. Note that Jensen in [Jen96] only describes substitution transitions and fusion of places, which were already described in [HJS91]. 3.5.1

Substitution places and transitions

The substitutions of transitions and places are based on the concept of page, the first explicit mechanism of static instantiation encountered in this document. A page is a CPN in which


14/34

some places and transitions have been marked as ports. CPNs are enriched with special entities called substitution transitions and substitution places. Each substitution place and transition is meant to be replaced by a copy of another page, thus bringing the notion of instantiation. These elements have a similar graphical notation to their standard counterparts, but they do not share their semantics: a substitution transition is not fired, its semantics are solely defined by the page that replaces them. There is another notion brought by substitution places and transitions that was not encountered in the previous formalisms: hierarchy among the components (see Section 2.4.2). Let us begin by describing substitution transitions. The places connected to a substitution transition are called sockets. During the composition, the substitution transition is replaced by the page it represents, and the sockets are merged to the port places in this page. This mechanism is pretty similar in its semantics to the place fusion mechanism seen earlier, with the difference that here the module interfaces are clearly defined. By using substitution transitions, the modeler can indicate that all the places in a place fusion set are going to be merged with places of the same page. Figure 6 shows an example of a substitution transition related to a subpage. The result of the composition is shown in Figure 7. Substitution places are very similar to substitution transitions. A substitution place is connected to another page that has some transitions marked as ports. The only real difference between substitution places and transitions is that more than one transition socket may be associated with the same port in the subpage. In this case, before merging the transitions, the port is duplicated as many times as it it necessary to ensure that one copy is going to be merged with each related socket. This is shown in Figure 8 and Figure 9, that show the composition of a page that has a substitution place related to another page. It is important to stress out that a page cannot be its own subpage: the hierarchy of pages forms a directed acyclic graph. The hierarchy of instances forms a tree. This is done to avoid infinite compositions. Declared interface Substitution transitions and places in the super-pages, transitions and places declared as ports in the sub-pages. Composition declaration Substitution nodes are related to other pages. The nodes around the substitution nodes are related to ports in the sub-pages.

Figure 6: A super page with a substitution transition, and the corresponding subpage taken from [HJS91]


Figure 7: The result of the composition of the two pages in Figure 6

15/34


16/34

Figure 8: A super page with a substitution place, and the corresponding subpage taken from [HJS91]

Figure 9: The result of the composition of the two pages in Figure 8 3.5.2

Invocation transitions

Invocation transitions are syntactically similar to substitution transitions. The key difference is that an invocation transition is replaced by the sub-page at runtime, i.e., during the execution of the net. This allows a page to be its own subpage, simulating a recursive procedure call in usual programming languages. The unfolding of invocation transitions may be infinite, in a similar way to recursive procedure calls, thus it is not always possible to build a non-modular CPN equivalent to a modular CPN with invocation transitions. Figure 10 shows and example of recursive invocation transition. The left page has an invocation transition that instantiates the right page called P ressCalc#6. In this right page, there are two possible executions: a simple execution, which is the terminating case and stops the ex-


17/34

ecution, and a complex execution, which creates itself two instances of P ressCalc#6 by means of the two transitions P C1 and P C2. Declared interface Similar to substitution transitions, there are special objects called substitution transitions in the super-page, and places labelled as ports in the sub-pages. Composition declaration An invocation transitions is replaced by the corresponding subpage at runtime. The places connected to the invocation transition are merged with the ports in the sub-page.

Figure 10: Example of a recursive invocation transition taken from [HJS91]


3.5.3

18/34

Fusion sets

Fusion sets in [HJS91] are very similar to the fusion sets we saw in the previous formalisms. The only difference is that they take into account the instantiation induced by the page hierarchy in substitution places and transitions, and invocation transitions. Thus, a fusion set can be local to a page, or global to all its instances across the system. Figure 11 shows a simple fusion set and its application to a page. Figure 12 shows the result if there is more than one instance of that page. At the left, the fusion set is marked as global, and at the right it is local to each instance. Declared interface None, all places and transitions can be merged. Composition declaration Place (resp. transition) fusion sets, that mark which places (resp. transitions) must be merged. This fusions sets may be marked as local or global.

Figure 11: Example of a fusion set taken from [HJS91]

Figure 12: Application of the fusion set of Figure 11 to two instances, globally and locally


3.6

19/34

Place/Transition refinements

In [ZB97], Zuberek and Bluembe propose a mechanism of modularity expressed as refinements. There is an initial standard P/T, and a set of refinement nets (also standard P/T). Places and transitions of the initial net may be refined by these refinement nets: the refinement net replaces the corresponding place (or transition), and the nodes that were connected to the original place (resp. transition) are connected to one or more nodes in the refinement net. With a heavy modification in the syntax, this could be boiled down to fusion of places and transitions. This modification is not trivial, as shown in the example shown in Figure 13. This figure shows two nets, one in the left and one in the right. Place P 2 in the left net is refined with the right net. Depending on the precise definition of the refinement, we could get one of the two results shown below. These two nets clearly have different behaviors. Declared interface None, all places and transitions can be refined. Composition declaration Complex functions between places, transitions and refinement nets. Note that [Feh93] defines the same kind of refinement, producing a formalism called Hierarchical Petri nets. The objective is to present the refinements in a hierarchical notation, allowing the visualization of the net at different levels of abstractions and the re-use of some sequences of refinements, but the underlying modular mechanism is the same as the one in [ZB97].

Figure 13: Two possible results for the refinement of a place


3.7

20/34

CP-nets with channels

In [CH94], Christensen and Hansen define an extension of CPNs called CP-nets with channels. CPNs are enriched with synchronous channels of communication. During their firing, transitions may read or write in these channels. A transition that writes a value in a channel is dynamically synchronized with a transition that reads from the same channel. If more than one transition reads from the same channel, any of them can receive the message, but only one of them will do it in a single firing. Thus, if two transitions {t1, t2} (from the same or from different nets) write in a channel, and three transitions {t3, t4, t5} read from the same channel, there are 6 possible executions: {t1t3, t1t4, t1t5, t2t3, t2t4, t2t5}. Note that each synchronization is performed between two and only two transitions: a writing transition and a reading transition. A translation from CP-nets with channels to CPNs can be performed with a duplication of transitions and a classical transition merge. Figure 14 shows an example of CP-net with channels, where two transitions write in a channel ch and two transitions read from the same channel. The writing transitions are labelled with the expression x!?ch, and the reading transitions with y?!ch. Figure 15 shows the flat CPN equivalent. Declared interface Transitions are enriched with expressions, indicating that they read or write in channels. Channels are declared as simple labels with a color type. Composition declaration Labels in the transitions give all the necessary information to make the composition. A transition writing in a channel is merged once will all the transitions that read from the same channel.

Figure 14: Example of CP-nets communicating through channels taken from [CH94]


21/34

Figure 15: The equivalent flat CPN of the nets in Figure 14

3.8

Composition of nets based on CSP semantics

In [Val93], Valmari proposed a formalism to compose P/Ts based on CSP semantics. Transitions are enriched with labels, and they are merged with transitions that share the same labels. A difference between this formalism and the CP-nets with channels is that here there is no notion of writing or reading from a channel, all the transitions that share a label are said to communicate among them. Thus, there are sets of transitions that are merged, instead of pairs like in CP-nets with channels. Figure 16 show three nets where all the transitions share the same label A, their composition is shown in Figure 17. Declared interface Transitions are enriched with labels, indicating that they are to be merged with transitions from other nets sharing the same label. Composition declaration Labels in the transitions give all the necessary information to make the composition. The transition fusion sets are the Cartesian product of the transitions that share a single label.

Figure 16: Three nets with all the transitions sharing a label


22/34

Figure 17: The result of the merge of the nets in Figure 16

3.9

Hierarchical High Level Petri nets

Buchholz presented in [Buc94] a formalism called hierarchical high level Petri nets (HHPN). Strictly speaking about modularity mechanism, this formalism is similar to the substitution places and transitions from [HJS91]. An HHPN is a hierarchical set of HLPNs that communicate through a set of ports. Graphically, each Petri net may contain internal modules represented by boxes with ports. A box in a net represents a communication with an inner or outer net. There are four kinds of ports: input place, output place, input transition and output transition. Place ports can only be connected to transitions and transition ports, and transition ports can only be connected to place and place ports. For the composition, output place ports from the outer-net are identified with input transition ports of the corresponding inner-net and output transition ports are identified with input place ports. This mechanism is best illustrated with a figure, shown in Figure 18. In that figure, there are three nets, Subnet0, Subnet1 and Subnet2. The upper-box in Subnet0 is identified with Subnet1. Whenever the upper-left transition of Subnet0 sends a value to the output place port, this value is sent to Subnet1. Then, the input transition port in Subnet1 places the value received in two places. The other connections work in a similar way. Note that, as HHPN work with HLPN, the values returned by the input ports may be the result of an operation computed on the value received by the corresponding output port. Declared interface Subnets are represented as boxes, and four kind of ports are added to ensure communication between outer and inner-components. Composition declaration A box in a net is matched with another net. Ports in the outer net are matched with ports in the inner net.


23/34

Figure 18: An example of HHPN taken from [Buc94]

3.10

Modular PNML

In [KP09], Kindler and Petrucci gave a formal definition of a modular formalism for Algebaic Petri nets (APNs) called Modular PNML, based on [KW01]. In this formalism, APNs are enriched with an interface, consisting in some places, transitions, sorts and symbols. For places and transitions, the composition mechanism is a simple fusion similar to the one in Modular CP-nets 3.1. Interface sorts and symbols are used to create modularity and encapsulation for data types. Thus, each module defines a set of data types, and when the modules are composed, their data types are also composed by means of signature homomorphisms. As most formalisms based on Algebaic Data Types (ADTs), there is a distinction between the specification of data types (their signature) and their implementation (the algebra). Modular PNML is a hierarchical formalism, in the sense that compound modules are defined over submodules, which can themselves be defined over their own submodules. Like in most hierarchical formalisms, the outer-module may have some places, transitions, sorts and operations that are not defined in any submodule. Each interface element is marked as imported or exported. Note that this import/export mechanism is a purely syntactical designation of "ownership" of the elements: a module that exports a place (resp. transition, sort or symbol) is the owner of that place (reps. transition, sort or symbol), a module that imports an element uses the respective element exported by another module. Thus, two places (resp. transitions, sorts and symbols) exported by two submodules cannot be merged, as each submodule would claim the "ownership" of the resulting merged place (resp. transition, sort and symbol). One important feature of this formalism in the context of this document is a formal definition of static instantiation, that is, the ability to indicate that a set of submodules are copies of a template. The only other formalism in this survey to explicitly define this feature is the


24/34

Hierarchical CP-nets. Note that [KW01] even defines a small and simple language to create a big set of instances of a module. Static instantiation is a central feature of any modular formalism. Figure 19 shows an example of a module in this Modular PNML, and Figure 20 shows a composition of three instances of this module inside an outer-module. Figure 21 shows the equivalent APN.

Figure 19: A module in Modular PNML taken from [KP09]

Figure 20: A composition in Modular PNML using static instantiation, taken from [KP09]

Figure 21: The flat Petri net equivalent to the one in Figure 20 Declared interface A set of imported and exported places, transitions, functions, and sorts. Composition declaration The imported and exported places and transitions of the submodules are merged with places and transitions of the outer module, taking care of keeping a consistent module. The data types modularity is defined by means of signature homomorphisms.


3.11

25/34

BIP

BIP (Behavior - Interaction - Priority) is a formalism presented in [BBS06] by Basu, Bozga and Sifakis. This is a general modular formalism adapted for various modeling formalisms. An instance of BIP for 1-safe P/Ts was presented in [BSS09] by Bozga, Sfyrla and Sifakis. In BIP for P/Ts, components are Petri nets enriched with variables and ports. Each Petri net transition is labeled with the name of a port, this means that each transition can only be fired if it is triggered by the corresponding port. A priority mechanism is defined as a strict partial order over ports. Compositions are declared by means of interactions. An interaction is a set of ports that denote the transitions to be synchronized. This synchronization is equivalent to a simple fusion of transitions. Composition also defines a new set of priorities for the compound module. Figure 22 shows a simple example of BIP composition.

Figure 22: A composition example in BIP taken from [BBS06] Declared interface A set of ports are added to the standard Petri net definition. From a pure Petri nets perspective, these ports could also be considered as labels on the transitions, but they have a graphical notation that stresses out the modularity of BIP components. Composition declaration The compositions are defined as interactions, i.e., sets of ports. The semantics of interactions are similar to transition fusion sets.

3.12

M-nets

Lilius defined in [Lil01] a formalism called M-nets. Syntactically, M-nets are high level nets with the particularity that places and transitions are enriched with labels and annotations. An important particularity is that these labels are parametric: a transition label may have a value that is unified with a value from an input arc. Thus, the transition labels are defined at runtime.


26/34

There are five compositions operations: parallel composition, transition synchronization, restriction, sequential composition and choice. Parallel composition is simply the disjoint union of two modules. Sequential composition and choice are similar to places merging, with some restrictions on the places to be merged, like in reentrant nets. Transition synchronization is the most complex operation. It is close to transition fusion, with three important particularities. • The fused transition is added to the existing transitions, instead of replacing them. Thus, the fusion of two transitions produces three transitions, the two original transitions and a third one resulting from the fusion. There is an additional operation, a restriction, that allows deleting some transitions along with its arcs. • A transition with a label A may be fused with any transition with the complementary label A. This mechanism can be related to the on used in CP-nets with channels from [CH94]. Nevertheless, unlike CP-nets with channels, a transition in an M-net may be synchronized with another transition from the same net, modeling recursive calls and leading to potentially infinite recursions. • The synchronization of the transitions takes the label of the transitions into account. As this label is parametric and depends on the values consumed and produced by the transition, the actual fusion is made at runtime. This leads to an eventual infinite unfolding of the net when building the corresponding flat net. The synchronization operation is briefly illustrated in Figure 23. It shows two M-nets (without any high-level labeling for simplicity reasons). The first one has a transition T 0 labeled with A0 . The second one has three transitions, T 1 with the label A, T 2 with the label A0 and T 3 without label. If both nets are synchronized and restricted over the labels A and A0 , the firing of T 0 is synchronized with the firing of T 1. Now, there are two possibilities: either T 3 is fired, and the net reaches a deadlock state, or T 2 is fired. As before, the firing of T 2 is synchronized with T 1, there is again a token in P 3 after the firing, and the same choice is presented again. Declared interface Labels in places and parametric labels in transitions. Composition declaration Five operations are declared: parallel composition, transition synchronization, restriction, sequential composition and choice. These operations have complex semantics, taking the place and transition labels into account.


27/34

Figure 23: An example of two M-nets to be composed by synchronization.

3.13 3.13.1

Communicative objects and cooperative nets Communicative objects

In [SB94], Sibertin-Blanc proposed two similar formalisms: communicative objects and cooperative nets. Both formalisms are object-oriented, where tokens may represent references to instances of HLPNs. As for all the object-oriented formalisms we describe in this document, communicative objects and cooperative nets have rather complex semantics, whose description goes well beyond our scope. We concentrate here on the modeling of modularity. Communicative objects are syntactically similar to standard HLPNs. A set of places are marked as accept-places. They are used to communicate messages (values) among instances of objects. Moreover, transitions are enriched with expressions. Two kinds of expressions are of interest to us: message sending and object creation. With an object creation expression, a transition can create new instances of a given object and set their initial values. With message sending expressions, transitions send values to accept places of other objects. This is illustrated in Figure 24. It is a very small excerpt of a philosophers model. Places Give and T ake are marked as accept places. The left transition takes a reference to a philosopher (which is another class, not presented here) from the place Give using the variable phil, and sends a message labelled phil.T akeLF ork(f ). In the philosophers class, there is an accept-place called T akeLF ork, that will receive the value f for the instance phil. Declared interface Some places are marked as accept-places. Transitions are labelled expressions that ensure the communication among objects. Composition declaration The labels of the transitions contain all the necessary information to perform the communication. The firing of a transition with a message sending expression puts a value in an accept-place of another object.


28/34

Figure 24: An example of communicative objects taken from [SB94] 3.13.2

Cooperative nets

[SB94] also presents cooperative nets, a formalism similar to communicative objects. In cooperative nets, objects communicate using a client-server protocol: a client requests a service by means of a request transition, the server accepts this request in an accept-place (these two mechanisms are similar to communicative objects). When the server has finished its work, it puts the answer in a return place. The client then executes a retrieve transition to retrieve the return value. Even though there is a conceptual difference between cooperative nets and communicative objects, the underlying semantic mechanisms are very similar. Declared interface Some places are marked as accept-places, others as return-places. Transitions are labelled expressions that ensure the communication among objects. Composition declaration The labels of the transitions contain all the necessary information to perform the communication.

3.14

Object colored Petri nets (OCP-Nets)

Maier and Moldt proposed in [MM01] an object-oriented formalism for CPNs called object colored Petri nets (OCP-Nets). It presents synchronous communications as fusion of transitions, and asynchronous communications with a mechanism very close to the one defined by cooperative nets. The client/server protocol is used for both types of communications. These communications are defined by means of special places (resp. transitions for synchronous communications): INV and REC places (resp. transitions) for the request and retrieval of a service, and IN and OUT places (resp. transitions) for the acceptance and return of a service. OCP-Nets also define a sub-typing relation is defined among components, which is a very powerful mechanism used in object-oriented languages. It is used to indicate in which circumstances some modules may be replaced by some other modules without affecting the behavior of the system. Figure 25 shows an example of synchronous communication in OCP-nets. The system represented is a stack, There are two transitions, IN and OUT, and a caller invokes these transitions using INV and REC transitions. Note that the label in the INV and REC transition indicate which instance of the stack receives the push request. Declared interface Some places and transitions are marked as INV, REC, IN and OUT. Moreover, they are also labelled with the name of the component that must receive the message, and the message itself.


29/34

Composition declaration The labels of the transitions contain all the necessary information to perform the communication.

Figure 25: An example of two synchronized object colored Petri nets taken from [MM01]

3.15

Object Petri nets

Lakos presented in [Lak01] an elegant formalism called Object Petri nets. It is another Objectoriented formalism: there is a notion of class and instantiation. An OPN class is composed by data fields, operations, transitions and arcs. Data fields are a generalization of places, merging the concepts of value, variable, and place in a single definition. OPN classes themselves are also data types. There are two distinct mechanisms for modularity: • Usual places and transitions are replaced by instances of classes. These instances may have themselves inner-OPNs, thus forming a hierarchy of nets. Syntactically, this composition is somehow similar to place and transition substitutions from [HJS91], but the semantics are more complicated, introducing both notions of synchronous and asynchronous communication. Figure 26 shows an example of this mechanism. Two classes are declared, U mbrella and Subscriber. Both have an interface that takes the form of arcs going to and from the edge of the class definition. • As for all object-oriented formalisms, references to objects may be passed as tokens. This implies a mechanism of dynamic instantiation. The exported data fields and operations of an object are accessible by means of expressions in the transitions and arcs. An example of this mechanism is to be found in Figure 27. A class called EDI system has a place


30/34

to store U mbrellas and another one to store Subscribers. umb (resp. sub) are instances of the objects from Figure 26. The firing of transition send takes a subscriber from place subscribers using the variable s. A guard (not depicted in the figure) unifies this variable with the class sub. Thus, the transition also takes a pair (0, d) from sub, which was a dynamically instantiated variable. Note that the concepts behind Object Petri nets go far beyond what is explained here (and far beyond the scope of this document). Declared interface Classes are represented as boxes, and arcs can go and come from this border, allowing communication. Moreover, classes have special elements declared as exported that may be accessible from transitions by means of labels. Composition declaration Classes are embedded inside outer-classes, forming a hierarchy similar to the page hierarchy from hierarchical CP-nets in [HJS91]. Exported data fields and operations are accessed by transitions by means of special labels in transitions.

Figure 26: An example of two object Petri nets taken from [Lak01]


31/34

Figure 27: An object Petri net composing the two nets from Figure 26

3.16

Concurrent Object-Oriented Petri Nets (CO-OPN)

In [BBG01] Biberstein, Buchs and Guelfi proposed the last formalism presented in this document, called CO-OPN/2. We first introduce a simplified version of the modularity used in CO-OPN/2, defined by Buchs, Costa and Hurzeler in [BCH02]. 3.16.1

A general component-oriented formalism

As BIP, the formalism presented in [BCH02] is not exclusive to Petri nets, but it can be instantiated for them. Similarly to BIP, this formalism defines a hierarchy of components. A component has an interface constituted by methods and gates. A method denotes a service offered by a component to its environment, and a gate denotes a service required by the component from its environment. Service calls are expressed as synchronous synchronizations. A gate from a component may be synchronized with a method from another component, to ask for the corresponding service. This synchronization is synchronous and transactional. The method call may modify the state of the given component. Moreover, a method may be internally synchronized with a gate from the same component to ask for another service to the environment. For two components to be synchronized, they must be embedded in an outer-component called a context. This outer component also has an interface with methods and gates. This is best illustrated with an example, shown in Figure 28. In that figure, two basic components model each one a simple buffer. These basic components are synchronized in order to model a bigger buffer. The basic components semantics may be defined with Petri nets (not represented in the picture). Each component has a method put to add a value in the buffer and get to retrieve a value. If the buffer is full, the put operation may fail. Instead of refusing the operation, the component uses a gate called f ailput to warn the environment of the situation. Note that the component itself does not know how the environment will treat the message send by the gate f ailput. Similarly, f ailget denotes a fail in the get method. The context represents the big buffer resulting from the composition of the two small ones. When the environment of the context requires a put service, this call is delegated to the put method of the left internal buffer. This buffer may accept the value, ending the execution of put,


32/34

or execute of the gate f ailput if it is full. This gate is synchronized with the method put of the second buffer. Thus, a refusal of the first buffer will delegate the call to the second buffer. Again, this buffer may accept the value, or execute its own f ailput gate. In the latter, as both buffers have failed to accept the value, the context executes itself its own f ailput gate, warning its own environment of this situation. All these operations are performed synchronously. Of course, the outer-buffer may itself by composed to other buffers to create bigger and bigger buffers. This example does not show the full power of this modular formalism. A gate may be synchronized with more than one method to ask simultaneously a service from different components. These composite synchronizations are defined with three operations: • parallel, where two methods or gates are called simultaneously. The semantics are similar to a fusion of transitions. • non-deterministic, where only one of the two methods is executed. • sequential, where two methods are executed one after the other transactionally, i.e., if the second method cannot be executed, neither can the first one. To the best of our knowledge, this mechanism cannot be represented in any other formalism presented in this document. Moreover, this formalism also defines the notion of mobility, where there are operations to move the inner-components from one context to another one, and create new synchronizations. This is illustrated in Figure 29.

Figure 28: Two synchronized buffers modeled as components, taken from [BCH02]


33/34

Figure 29: Component mobility example taken from [BCH02] Declared interface Modules have an interface composed of methods and gates. Composition declaration Methods and gates are transactionally composed by means of three operators: parallel, non-determinism and sequential. 3.16.2

CO-OPN

CO-OPN/2, described in [BBG01], uses the concepts of the previously described modular formalism to create an object-oriented formalism based on APNs. Objects have an interface composed of methods (later works added the notion of gate to distinguish incoming from outgoing requests). Objects are organized in a hierarchical way, with objects located inside other objects. Two objects in the same context may be synchronized using the three previously defined operators. Moreover, similarly to the previous object-oriented formalisms, the tokens can be references to objects, and the methods and gates of the objects may be accessed by means of expressions in the transitions. There is also a dynamic instantiation mechanism. The are many more details about the semantics of CO-OPN/2 that are not mentioned in this document. Declared interface Classes have an interface composed of methods and gates. Composition declaration Methods and gates are transactionally composed by means of three operators: parallel, non-determinism and sequential. Moreover, methods and gates may be accessed when executing transitions, using the object references as tokens.

4. CONCLUSION

4

34/34

Conclusion

This document sketches a state of the art of the modular formalisms in the Petri nets literature. 17 different formalisms were informally described, mainly through the use of small examples. Classification criteria were used to analyze some common characteristics among them. These characteristics include syntactic concerns, such as the definition of an interface for the modules, and semantic concerns such as the possibility to dynamically instantiate modules. We observed in this document that modularity is represented by a wide range of very different mechanisms. Even though some of these mechanisms are relatively close to each other from a semantics point of view, usually the corresponding concrete syntaxes are extremely variable. Some of these mechanisms are rather simple and intuitive, while others bring more complex concepts. The most complex formalisms observed are the object-oriented ones: they bring extremely powerful modeling concepts to the Petri net models, but they sacrifice the simplicity of the original Petri nets formalism. A single definition for all these mechanisms would clearly be an extremely difficult task. To overcome this difficulty, one may be tempted to reduce the characteristics considered, e.g., by only considering place and transition fusion sets. This may reduce the modular formalisms zoo to a manageable size, at the cost of ignoring important concepts.

REFERENCES

References [BBG01]

Olivier Biberstein, Didier Buchs, and Nicolas Guelfi. Object-oriented nets with algebraic specifications: The CO-OPN/2 formalism. In G. Agha, F. De Cindio, and G. Rozenberg, editors, Advances in Petri Nets on Object-Orientation, LNCS, pages 70–127. Springer, 2001.

[BBS06]

Ananda Basu, Marius Bozga, and Joseph Sifakis. Modeling heterogeneous real-time components in bip. In Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods, pages 3–12, Washington, DC, USA, 2006. IEEE Computer Society.

[BCH02]

Didier Buchs, Sandro Costa, and David Hurzeler. Component based system modelling for easier verification. Concurrency in Dependable Computing, pages 61 – 86, 2002.

[BSS09]

Marius Dorel Bozga, Vassiliki Sfyrla, and Joseph Sifakis. Modeling synchronous systems in bip. In Proceedings of the seventh ACM international conference on Embedded software, EMSOFT ’09, pages 77–86, New York, NY, USA, 2009. ACM.

[Buc94]

Peter Buchholz. Hierarchical high level petri nets for complex system analysis. In Robert Valette, editor, Application and Theory of Petri Nets 1994, volume 815 of Lecture Notes in Computer Science, pages 119–138. Springer Berlin / Heidelberg, 1994.

[CF10]

Thomas Chatain and Eric Fabre. Factorization properties of symbolic unfoldings of colored petri nets. In Petri Nets, pages 165–184, 2010.

[CH94]

Søren Christensen and Damgaard Hansen. Coloured petri nets extended with channels for synchronous communication. In R. Valette, editor, Lecture Notes in Computer Science; Application and Theory of Petri Nets 1994, Proceedings 15th International Conference, Zaragoza, Spain, volume 815, pages 159–178. Springer-Verlag, 1994.

[Che91]

Ghassan Chehaibar. Use of reentrant nets in modular analysis of colored nets. In Grzegorz Rozenberg, editor, Advances in Petri Nets 1991, volume 524 of Lecture Notes in Computer Science, pages 58–77. Springer Berlin / Heidelberg, 1991.

[CP92]

Søren Christensen and Laure Petrucci. Towards a modular analysis of coloured petri nets. In Proceedings of the 13th International Conference on Application and Theory of Petri Nets, pages 113–133, London, UK, 1992. Springer-Verlag.

[CP00]

Søren Christensen and Laure Petrucci. Modular analysis of petri nets. Comput. J., 43(3):224–242, 2000.

[Feh93]

Rainer Fehling. A concept of hierarchical petri nets with building blocks. In Papers from the 12th International Conference on Applications and Theory of Petri Nets: Advances in Petri Nets 1993, pages 148–168, London, UK, 1993. Springer-Verlag.

[HJS91]

Peter Huber, Kurt Jensen, and Robert M. Shapiro. Hierarchies in coloured petri nets. In Proceedings of the 10th International Conference on Applications and Theory of Petri Nets: Advances in Petri Nets 1990, pages 313–341, London, UK, 1991. SpringerVerlag.

[Jen96]

Kurt Jensen. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. Volume 1. Springer Publishing Company, Incorporated, 1996.

REFERENCES

[KP09]

Ekkart Kindler and Laure Petrucci. Towards a standard for modular petri nets: A formalisation. In Proceedings of the 30th International Conference on Applications and Theory of Petri Nets, PETRI NETS ’09, pages 43–62, Berlin, Heidelberg, 2009. Springer-Verlag.

[KW01]

Ekkart Kindler and Michael Weber. A Universal Module Concept for Petri Nets — an implementation-oriented approach, 2001.

[Lak01]

Charles Lakos. Object oriented modeling with object petri nets. In Concurrent Object-Oriented Programming and Petri Nets, pages 1–37, 2001.

[Lil01]

Johan Lilius. Ob(pn)2 : An object based petri net programming notation. In Concurrent Object-Oriented Programming and Petri Nets, pages 247–275, 2001.

[MM01]

Christoph Maier and Daniel Moldt. Object coloured petri nets - a formal technique for object oriented modelling. In Gul A. Agha, Fiorella De Cindio, and Grzegorz Rozenberg, editors, Advances in Petri Nets: Concurrent Object-Oriented Programming and Petri Nets, LNCS, pages 406–427. Springer, 2001.

[SB94]

Christophe Sibertin-Blanc. Cooperative nets. In Proceedings of the 15th International Conference on Application and Theory of Petri Nets, pages 471–490, London, UK, 1994. Springer-Verlag.

[Val93]

Antti Valmari. Compositional state space generation. In Grzegorz Rozenberg, editor, Advances in Petri Nets 1993, volume 674 of Lecture Notes in Computer Science, pages 427–457. Springer Berlin / Heidelberg, 1993.

[Val94]

Antti Valmari. Compositional analysis with place-bordered subnets. In Proceedings of the 15th International Conference on Application and Theory of Petri Nets, pages 531–547, London, UK, 1994. Springer-Verlag.

[ZB97]

W. M. Zuberek and I. Bluemke. Hierarchies of place/transition refinements in petri nets. In in Proc. Conference on Emerging on Technologies and Factory Automation, pages 355–360. B b, 1997.

[ZHLR95] Job Zwiers, Ulrich Hannemann, Yassine Lakhnech, and Willem P. de Roever. Synthesizing different development paradigms: Combining top-down with bottom-up reasoning about distributed systems. In Proceedings of the 15th Conference on Foundations of Software Technology and Theoretical Computer Science, pages 80–95, London, UK, 1995. Springer-Verlag.

REFERENCES

SMV Technical Reports This report is in the series of SMV technical reports. The series editor is Didier Buchs (Didier. [email protected]). Any views or opinions contained in this report are solely those of the author, and do not necessarily represent those of SMV group, unless specifically stated and the sender is authorized to do so. You may order copies of the SMV technical reports from the corresponding author or the series editor. Most of the reports can also be found on the web pages of the SMV group (http://smv.unige.ch/).

Abstract Modularity in Petri nets is an important topic that has been studied for years. It is a mandatory principle for using Petri Nets in real size systems and also to promote reuse. Indeed, the introduction of high level nets solves the question of modeling multiple similar behaviors. However, modularity principles are needed to handle the heterogeneity of the concepts to model by using a divide and conquer approach. Although important to study, modular principles have been difficult to settle in the Petri net domain. A naive approach is to consider a syntactic approach, where modules have to be composed to create a single Petri net to compute the behavior. The prevailing approach is a semantic approach, where each module has its own semantics defined prior to composition. There exists a large variety of composition mechanisms such as place fusions, transition fusions and synchronization mechanisms. Synchronization mechanisms are the more elaborated way of linking modules. They may be asynchronous or synchronous and may impose transactional or atomicity principles. An additional dimension is present in the object-oriented approach, when modules are dynamically created and referenced. This document is an attempt to make a state of the art in the domain of modularity for Petri nets. The main objective is to stress out the vast array of modular mechanisms that have been defined over the years instead of exploring all the existing modular formalisms. Keywords: Petri Nets, Modularity, Composition, Object-oriented