3. Describing Interfaces by means of Petri-nets

[About Petri-nets] Where is ``Start'' ??
- Dirk van Deun

WHEN WE WANT TO AUTOMATICALLY GENERATE an adaptor between conflicting interfaces, the program that generates the adaptor needs some knowledge about the interfaces required and provided. This chapter introduces a formal technique to specify interfaces. Specifically we will investigate the use of Petri-nets as a formal documentation technique.

3.1 Introduction

AS EXPLAINED IN PREVIOUS CHAPTER every component has a number of ports. Every port embodies a certain behavior. This can be compared with the interface offered by objects in an object oriented language. This interface, typically called an application program interface (or API for short), must be documented before someone can use the functionality offered by that interface.

Often this API is nothing more than a standard listing of method-signatures. This is clearly insufficient for our purposes for two reasons. Firstly, method signatures have semantics incompatible with the semantics of our ports because we are working in an event based model in which 'messages' are transmitted between components. This implies that messages are passed by value and that a message not necessarily specifies that a certain method needs to be called. A message can be for instance something like $(12,13)$. Lastly, messages, in comparison to standard method calls, will never return a value. Therefore a simple list of method signatures is not very well suited to document ports. A second reason why common used API's are not suitable is that method signatures do not specify enough information to allow a program to extract interesting properties. This, we will show, is necessary in order to generate an intelligent adaptor. Therefore we will now investigate which technique is usable to formally document an interface.

3.2 Formal Interface Descriptions

COMMONLY USED FORMAL SYNTACTICAL INTERFACE DESCRIPTIONS simply state what methods can be called, with which parameters. Sometimes a type system specifies what kind of objects need to be passed. Specifying interfaces this way suits compiler and linker, and together with an informal explanation of what the interface is supposed to do, can be understood by humans. For machines, on the other hand, there is a lot of information missing within such a simple syntactical description.

• They do not specify in what order certain methods can be called. This is an important drawback because, without this information an number of possibilities is left open. Possibilities that almost always result in wrong behavior or errors. E.g.: a computer simply doesn't know when a message Init should be sent. A human might immediately start by thinking to send an Init at the beginning and a Done message at the end of some action.
• Most of the time formal syntactical interface descriptions only state what they provide to a client, they seldomly specify what is required from the client. Implicitly the client knows it must be able to handle the return values. In a non-blocking systems on the other hand it is commonplace to use callback messages. These are often specified in an ad hoc way. For example, a whiteboard can decide autonomously to send a HasDisjoined() message to the client.
• Session behavior is almost never specified. Typically a programmer expects an interface to be called only by him. In a non-blocking system an interface may need to process messages in an unknown order. Whether this is possible and how this is managed is also never specified. For example, whether some messages are kept aside and will be processed later is very difficult to express in a formal way.

It is important to observe that the only reason why we are nowadays using formal syntactical interface description is because compilers need them. Without them, compilers nor linkers would be able to do either type checking or linkage of two interfaces.

Now, let us think about machines that need to understand interfaces. It is obvious that they cannot make much more sense out of simple API's than they already do (that is type checking and linking). If we want to create an adaptor, then a machine needs to understand enough of the possibilities offered by an interface. Therefore we will do what is typical done is such situations: specify this extra information in a formal way.

The problem that arises now is that, contrary to a syntactical description it is difficult to capture the semantics of an interface. How far should we describe the interaction ? Should we only describe when a certain function can be called or do we also need to specify what the arguments should look like ? If we would specify what the arguments look like do we need to specify the maximum and/or minimum size of the data transferred ? In short, it is very difficult to describe an interface in a formal way without capturing too much detail, or without giving a trivial description (such as: this function will be called at some time). The programmer should have the freedom to specify what he wants in an easy formal way. The formalism should not stop him from expressing certain requirements, it should be flexible and easy to understand. Therefore, the formalism we will use are Petri-nets.

3.3 Petri-Nets

THE FORMALISM WE WILL USE TO SPECIFY THE BEHAVIOR of an interface will be colored Petri-nets. Petri-nets were originally invented by Petri[Pet62]. Petri-nets have a number of very appealing properties. For an in-depth discussion of all these properties see [KCJ98].

1. They are specified by means of a graphical representation. A representation that is intuitive and covers in one drawing enough detail to understand what the represented model is about.
2. Petri-nets have a description of both states and actions, this in contrast to state diagrams or transition diagrams, which cover only part of the behavior of a system.
3. Colored Petri-nets include data manipulation within the Petri-net. A colored Petri-net covers state transition, state of a system and data manipulation in one drawing.
4. Petri-nets are a formalism that can describe a system at any level of abstraction. Petri-nets can be used to describe the interaction between high level modules as well as the full interaction within these modules. Petri-nets can specify a large variety of different systems. This can be illustrated by pointing out the number of practical situations in which Petri-nets have helped. see [KCJ98]
5. The basic building blocks of Petri-nets are places, transitions (and tokens for colored Petri-nets). These primitives are easy to understand and very powerful.
6. Petri-nets allows modularization of systems by means of hierarchical decomposition. Petri-nets can be combined using certain operators, which we will not discuss here. For more information see [BFF⁺95a].
7. For real time systems and timed distributed systems, Petri-nets can be extended with a time concept. See [PM93,BMAPY97].
8. Petri-nets are stable with respect to minor changes of the modeled system. This is illustrated by many practical experiences. It means that small modifications of the modeled system does not require a complete rewrite of the Petri-net. In many other description languages this is not the case (e.g.: finite automaton).
9. Petri-nets can be formally analyzed. This means that certain properties of the modeled system can be verified. This includes: construction of occurrence graphs (which global states are reachable), calculation of invariants (pre- and post- conditions checking), reductions (shrink down a Petri-net but still preserve a number of properties) and checking of structural properties (such as starvation).

A large drawback of Petri-nets nowadays is that there is essentially only a graphical notation which is agreed on. A notation in text-format, which is absolutely necessary, is difficult to find and certainly there is no agreement on such a notation. At the end of this chapter we will introduce our own notation, which suits our needs, but before we continue our Petri-net investigation we will look at some other existing techniques.

3.3.1 Related work

It is very difficult to find a formal documentation technique that is a) as general and formal as Petri-nets and b) as useful as Petri-nets at the same time. Below we will shortly touch upon a number of techniques to do so.

3.3.1.1 State Machines

Finite automatons (FSM's) and state diagrams [Har87,JMW⁺91,G.01] have problems when multiple concurrent sessions should be expressed and their size explodes very quickly with every newly added behavior.

3.3.1.2 Reuse Contract

Reuse Contracts [LSMD96], invented at the Programming Technology lab of the VUB, are a means to describe the behavior of an interface in an abstract way. This abstract interface description is called a reuse contract. From reuse contracts a number of properties of an implementation can be deduced, for instance reuse contracts can help in evolving a software system such that existing software dependent on the framework still functions as expected. The approach described in [LSMD96] has some drawbacks, which also form the reason why we didn't use them in our work:

• Reuse contracts describe the behavior of non concurrent objects, not the behavior of concurrent components. Whenever faced with concurrent processes the formalism might not be suitable anymore.
• Reuse contracts only specify what is provided, barely what is required from another interface.
• The level of detail cannot be chosen easily without braking the deductive power.

3.3.1.3 Message Sequence Charts

Message sequence charts (MSC's) [JCJO92,Wyd01], as a documentation technique, offers example traces of what a component can do. However, message sequence charts typically documents only one run through a component and are difficult to extend to include all possible traces of a component. A second drawback of the work presented in [Wyd01] is that it is only possible to reason about the sequence of things to happen, not about the actual content of the data transmitted. For concurrent systems this is a large drawback. It is almost completely impossible to describe the semantics of a rollback-able transaction without taking the state of the resources into account.

3.3.1.4 Pure logical approaches

The use of purely logical approaches that specify what conditions should be met would be possible: it is not too difficult to use predicate-logic or proposition-logic to describe the behavior of an interface to a chosen level of detail. Often this is done by using pre- and post-conditions to describe when a message can be send or received. However, since these approaches are barely readable and do not offer extra advantages over Petri-nets we chose not to use them to describe the behavior of component interfaces.

3.3.1.5 Temporal logics

The use of temporal logics [KV97,Pnu77] to describe when which transition is enabled could also have been possible. Again the drawback here is the readability and the difficulties one can have to write down even simple statements such as: 'between every occurrence of $A$ and $B$ there can only be one enable or disable transition'.

3.3.1.6 SDL

Another, well known specification technique such as SDL [OFM97,JDA97], which is widely used to specify communication protocols, can be easily mapped onto Petri-nets [FG98].

3.3.1.7 IDL's

The lack of a formal semantical description of interfaces in protocols has been recognized for a long time. See [Bra01]. In the past, attempts have been made to extend CORBA IDL's with extra formal specifications in such a way that they could help in automatic checking of the protocols involved [CFP⁺01]. However, since we are not working with IDL's anyway there was no use in using these approaches. [BOP] discusses how Petri-nets can be used to describe the behavior of CORBA objects.

3.3.1.8 Existing Petri-net tools

A lot of tools support Petri-net in all kinds of contexts. The main reason why we didn't use them is because we are using Petri-nets in a context in which they are generated automatically. This includes a random element and by generating pseudo-random Petri-nets we would test every tool to its limits. It is not to be expected that a tool which survives all possible Petri-nets will be found quickly. Neither would it be possible to fix bugs in such a tool because most often the source is not free. A second reason why existing Petri-net tools have not been used is that most of the existing tools are to be paid for.

However, there is one tool we did investigate because it looked very promising: Pep. Pep [Gra] is a programming environment, developed at the university of Oldenburg by the parallel systems group and is based on Petri-nets in which the programmer can design the requirements of a parallel system using a process algebra notation, called $B(PN)^{2}$ [BH93], SDL[OFM97], high level Petri-nets, called M-nets, or low level petri-nets. Along with the tool comes a set of compilers which generate Petri-nets from the different kinds of input formats. A lot of papers have been published how certain of these languages can be mapped onto Petri-nets [BFF⁺95b,FG98]. The Petri-nets can be visually simulated, and the possibility exists to link it with a 3D VRML environment. Automatic verification is also included in Pep, by means of an integration of other packages such as an Integrated Net Analyzer, a symbolic verification system (developed at CMU) and others.

Pep's big attraction is due to the good programming documentation and documented internals. The whole abstract Petri-net notation is given in an understandable form. Its drawbacks on the other hand are its incorrect conversion from high level petri-nets to low level petri-nets and its wrong execution of high level petri-nets. It seems as if every high-level place acts as a queue on which messages can come in and whenever a transition needs to be checked only the top level elements are checked. In most cases this is suitable and this is certainly suitable if the Petri-nets are generated automatically. However, a suitable combination of tokens, such as is required from colored petri-nets, is not the case, which makes executing an automatically generated Petri-net an impossible case. Another drawback of Pep is that its Petri-net file format is very rigorous and unreadable. Specifying a Petri-net is difficult because there are cross-linked labels and references almost everywhere. This is something which is a) unnecessary and b) difficult to keep track of when specifying a Petri-net.

A second tool we wanted to investigate, is CPNet. This is the tool promoted by the author of [Jen94], is sold to companies and is supposed to be free for universities. However after contacting the authors 3 times we still didn't get any answer.

3.4 Colored Petri-Nets

Figure 3.1: A Petri-net describing a non-nested locking strategy.

PETRI-NETS ARE OFTEN DRAWN AS BOX/CIRCLE DIAGRAMS. Figure 3.1 is a box/circle diagram of a Petri-net describing the behavior of a non-counting semaphore. Petri-nets have a number of concepts:

• Places: places represent the state of a system. In our example, these are the circles. The places are Unlocked, Unlocking, Locking, Locked and Acting.
• Tokens: A place can have zero, one or more tokens. Simple Petri-nets only have boolean tokens. A token is either there or is not there. In our example only the Unlocked place contains a token. Tokens which contain values will be discussed when we describe colored Petri-nets.
• Transitions: A transition specifies how a token is moved from one place to another. In our example, we have the transitions: UnlockDone, Lock, LockFalse, LockTrue, Unlock, ActDone and Act. A transition can be either enabled or disabled. If all the arcs coming into a transition offer a token the transition is enabled. In our case only the transition Lock is enabled because the only incoming arc from Unlocked offers a token. The transition Unlock is not enabled since there is no token at Locked. When a transition is executed all offered tokens, that take part in enabling the transition, are taken away from their place and transferred to all the places that receive an arc from this transition. If we would execute the transition Lock the token would be moved from Unlocked to Locking. Afterward the transition LockFalse and LockTrue will be enabled.
• Marking: The marking of a Petri-net contains all the places that contain a certain token. The marking is in fact the global state of a Petri-net. It is perfectly possible to have a Petri-net in which multiple places contain a token.

The previous description describes the elementary properties of Petri-nets. Although enough to describe the basic operation of a Petri-net, colored Petri-nets allows tokens to carry a certain value. This small extension to Petri-nets complicates the formalism a lot. It is not clear when a certain transition is enabled: can we specifically check the color of a token or do we only check its presence. It is also not clear what should happen when a transition is executed, what color/value will the outgoing token(s) have ? Is it possible to send different tokens to different places ? Below we will explain how colored Petri-nets are defined.

3.4.1 Informal Discussion

Figure 3.2: A colored Petri-net illustrating a nested locking strategy for a whiteboard of 32x32 squares.

From an informal point of view a colored Petri-net consists of places, transitions, a relation in between them and expressions which are used to verify incoming tokens/values and create new tokens/values. The Petri-net in figure 3.2 illustrates what an easy to understand colored Petri-net looks like for a nested locking strategy in a whiteboard containing 32x32 squares. A number of additional properties can be observed:

• First, every place has a type associated with it, a color set. This type declares which possible values can be present at the given place. For instance the Locking place has a type/color $X\times Y\times C$. $X$ is the set of possible X values $[0..31]$, $Y$ is the set of possible Y values $[0..31]$ and $C$ is the set of possible lockcounts, $[0..\infty[$. The possible colors of the tokens, or values for short, at the locking place are tuples which belong to the set $X\times Y\times C$. The values $(0,0,0)$, $(31,5,900)$ are valid tokens, while the values $(-1,0,0)$, $(32,5,900)$ are invalid tokens.
• Second, places can contain more than one token.
• Third, all arcs contain an expression which either describes the tokens generated or the tokens to be matched. From the point of view of a transition
  • every incoming arc describes which tokens are looked for. For example, the incoming arc on the LockTrue transition needs a 3-tuple, if one is available, such as $(10,10,0)$ the variables $X$, $Y$ and $C$ will be bound to the values present in the token/tuple. So, $X=10;Y=10;C=0$.
  • every outgoing arc describes how new tokens are generated. If the LockTrue transition is executed all incoming tokens are removed from the input places and the output places receive newly created tokens. For example, the outgoing arc of the LockTrue transition contains the expression $(X,Y,C+1)$. Since the variables $X$, $Y$ and $C$ were bound to $10$, $10$ and $0$, the new token will be $(10,10,1)$. This token will be put in the place LockCount.
• Fourth, some transitions can contain guards. A guard is an expression which verifies whether the transition is enabled given a number of input tokens. A guard is also an expression in some sort of language, which will be described later. A guard should evaluate to true or false. When a guard evaluates to true the transition is enabled, when the guard evaluates to false but still all tokens are present the transition is not enabled. For example, the transition Unlock has a guard $C>0$. Intuitively this means that a lock cannot be released if the lock is not held. The outgoing arc of the UnlockDone transition has an expression $(X,Y,C-1)$ which decreases the lock counter with one. Because we are sure that the incoming token has a lockcount larger than $0$, the resulting token will always be in the set $X\times Y\times C$.
• Fifth, the expression language used within guards and on arcs can be chosen. However if one chooses a language too rigorous (Turing complete) a lot of analyzing power might be lost. The language we will choose will be described below.

Figure 3.3: A nested locking strategy upon a squared whiteboard with only one place.

Given this, we can now clearly see the expressive power of Petri-nets. We can choose how much detail we include in our Petri-net. The Petri-net given in figure 3.2 only covers the locking of a single square with a lockcount. If we want we could add a session ID to check whether the incoming lock request is from the same one who already has obtained a lock. The fact that we do not need to specify this, without losing the ability to reflect over the behavior of the system is one of the greatest strengths of Petri-nets.

It is even possible to describe the same behavior with only one place. Therefore we need to add another color $B$ which describes whether a certain position is in busy locking (busyL), busy unlocking (busyU) or available (avail). The associated Petri-net, without acting logic for the sake of simplicity is pictured in 3.3. On the other hand if we need to use this Petri-net in a larger context, in which we only need to know whether a place is locked or unlocked we can split the LockCount state of figure 3.2 in two as depicted in figure 3.4.

Figure 3.4: A large Petri-net describing the behavior of a nested locking strategy on a whiteboard consisting of 32 x 32 squares. There are separate states for 'unlocked' and 'locked'. When locked a lock counter is kept.

Simple Petri-nets, which we will need later on, are Petri-nets in which tokens cannot contain a color. They only can be at a certain place. A simple Petri-net only allows for one token per place. A simple Petri-net also doesn't have guard, input or output expressions.

3.4.2 Formal Definition

We will now define Colored Petri-nets formally. The definition given below is based, to a large extent, on the well known work of [Jen94]. Mainly we have removed some $name\rightarrow place$ and $name\rightarrow transition$ mappings, however this does not modify the formalism it merely simplifies it for our purposes. The often-used and referenced definition given in [Jen94] is not the first definition given of colored Petri-nets, other definitions also exists such as referenced in [EK98,Lak94]. However, they are not explained in as much detail as the one we will use.

Before we can explain the details of colored Petri-nets we need the ability to describe multiple tokens at the same place. Since this is something that cannot easily be expressed with mathematical sets, we resort to multi-sets.

A multi-set is a set in which every element can occur multiple times. Formally a multi-set $m$ is defined over a certain underlying set $S$ as a function that maps every element of S to a natural number: $m:S\rightarrow\aleph$. The domain of the multi-set: the occurency counts of every possible element of $S$ are called the coefficients of $m$. All possible multi-sets associated with a certain set $S$ will be denoted as $S_{MS}$. This should not be confused with the power-set, denoted $2^{S}$ which is the set of all possible subsets.

A second preliminary before we can explain the formal side of colored Petri-nets concerns expressions. The guards and actions work on values. The way in which these are represented is currently left open, any type of expression can be inserted into a colored Petri-net. For example, one can use $\lambda$ expressions, or simple algebraic expressions. One can choose whatever fits best. If one chooses a language too expressive a certain level of formal analysis will no longer be possible. We will discuss this later on. Once one has chosen an expression language one cannot change this anymore within the same Petri-net. In the following definitions we will refer to an expression as $expr$. $Expr$ (with a capital) refers to all possible expressions. For every expression $expr\in Expr$ it should be possible to obtain the type and free variables. We should also be able to evaluate it under a certain binding of values to variables:

• A type is a finite or infinite set of possible values. For example, a type can be a set such as $\{0,1,2,3,4,...\}$ or it can be a set such as $\{'aaa','aab','aba','abb',...\}$. The boolean type: $\{\textrm{true},\textrm{false}\}$ will be referenced to as 'bool'.
• $Vars:Expr\rightarrow Var$ is a function that returns the set of unbound variables within $expr$.
• $Type:Expr\rightarrow Type$ returns the set of possible values (the type) an expression can return.
• A binding $b$ of a set variables $V$ associates with each element $v\in Var$ an element out of $Type(v)$, such that $b(v)\in Type(v)$.
• The value of an expression $expr$ under a certain binding $b$ is denoted as $expr\langle b\rangle$. The expression is reduced similar to $\lambda$-calculus by substituting every variable $v\in Vars(expr)$ with the value $b(v)$.

We are now ready to define a colored Petri-net formally:
A CPNet is a tuple $N=(\Sigma,P,T,A,C,G,E,I)$ where

• $\sum$ is a non empty set of types, called color sets.
• $P$, $T$, $A$ are the places, transitions and the flow relation between places and transitions. $P\cap T=P\cap A=T\cap A=\phi$. The flow relation A contains tuples from $P\times T\cup T\times P$. This is in contrast to the definition given in [Jen94], in which a node-function is added to the Petri-net which maps an arc to such a tuple. This small change however doesn't change any semantics associated with the net as explained in [Jen94].
• $C:P\rightarrow\Sigma$ is a color function. This function associates a type with every place. All tokens present at a place $p$ must be of type $C(p)$.
• $G:T\rightarrow Expr$ is a guard function if $\forall t\in T:(Type(G(t))=\textrm{bool }\wedge Type(Var(G(t)))\subseteq\Sigma)$. Informally speaking, we associate with every transition an expression. This expression should result in a boolean type and all variables used within the expression should require a known type, thus be part of $\Sigma$.
• $E:A\rightarrow Expr$ is an arc expression, or action: such that $\forall a=(p,t)\in A\vee a=(t,p)\in A:(Type(E(a))=C(p)_{MS}\wedge Type(Var(E(a)))\subseteq\Sigma)$ where the place $p$ the associated place of $a$ is. The arc expression associates with every arc an expression, which will be used to verify or create new token-values. Every arc expression should evaluate to a set of tokens (a multi-set over the different types allowed by the place). $E$ contains input expressions as well as outgoing actions.
• $I:P\rightarrow Expr$ is an initialization function such that $expr\in Expr$ has no free variables and $\forall p\in P:Type(I(p))=C(p)_{MS}$

Table 3.1: A Petri-net $(\Sigma P,T,A,C,G,E,I)$ of the Petri-net pictured in figure 3.3. The tuple-elements $C,G,E$ and $I$ are functions denoted as a set of couples.

$\Sigma$

$\{ XY=\{0,1,2,...,31\},C=\{0,1,2,...\},B=\{ busyL,busyU,avail\}\}$ $P$

The above describes the static structure of a CPNet. Figure 3.1 describes in a formal way the the Petri-net pictured in figure 3.3.

To describe the dynamic behavior of a CPNet we will first describe what a marking is, then describe when a transition is enabled and finally what happens when a transition is executed. But before we do so, some syntactic sugar is introduced.

• $A(t)=\{ a\in P\times\{ t\}\cup\{ t\}\times P\}$ which returns the arcs associated with the transition t.
• $Vars(t)=Vars(G(t))\cup\{ v\vert\exists a\in A(t):v\in Vars(E(a))\}$

A binding of a transition $t$ is a function $b$ such that

$$G(t)\langle b\rangle \wedge \forall v\in Vars(t):b(v)\in Type(v)$$

The set of all bindings for $t$ is called $B(t)$. A token element is a couple $(p,c)$ with $p\in P$ and $c\in C(p)$. A binding elements is a couple $(t,b)$ with $t\in T$ and $b\in B(t)$. The set of all possible token elements is called $TE$, the set of all possible binding elements is called BE. Now we can define a marking:

A marking is a multi-set over $TE$. The initial marking $M_{0}$ is obtained from $I$ as follows

$$\forall(p,c)\in TE:M_{0}((p,s))=(I(p))(c)$$ (3.1)

A transition $t$ is enabled if a) there exist a binding satisfying the guard ($b\in B(t)$) and b) all expressions placed on the incoming arcs result in something of the correct type. We will denote this as $M[t\rangle$, which specifies that transition $t$ is enabled under marking $M$. Formally,

$$M[t\rangle\iff\exists b\in B(t):\forall(p,t)\in A:E((p,t))\langle b\rangle\leq M(p)$$ (3.2)

During the rest of the dissertation we will us a shorthand notation $M^{\bullet}$ to specify the set of all enabled transitions under marking $M$.

$$M^{\bullet}=\{ t \vert M[t\rangle\}$$

$M^{\bullet}$ will be called the postcondition of $M$. When an enabled transition $t$ is executed (fired) the marking $M_{i}$ changes to $M_{i+1}$as follows :

$$M_{i}[t\rangle M_{i+1}\iff\forall p\in P:M_{i+1}(p)=M_{i}(... ...{(t,b)\in BE}E((p,t))\langle b\rangle+E((t,p))\langle b\rangle$$ (3.3)

A shorthand notation $M^{\bullet\bullet}$ will be used to denote the set of all possible future markings after firing one of the enabled transitions.

$$M^{\bullet\bullet}=\{ N \vert \exists t : M[t\rangle N\}$$

For both shorthand notation, $M^{\bullet}$and $M^{\bullet\bullet}$, which both specify what can happen next, two other notations exist, which describe what could have happened before. $^{\bullet}M$ is called the pre-condition of $M$.

$$^{\bullet}M=\{ t \vert \exists N : N[t\rangle M\}$$

$$^{\bullet\bullet}M=\{ N \vert \exists t : N[t\rangle M\}$$

3.4.3 Simple Petri-Nets

The above formal definition of Colored Petri-nets can be scaled down to Elementary Place Transition nets. To do so, the concept of multiple tokens per place, different colors per token and (input-, output- and guard-)expressions has to be removed. The resulting net has almost the same dynamics as a colored Petri-net, however, because only one token is allowed per place, a transition is only enabled when none of its output places contains a token.

3.4.4 A Note on Implementation

Below we explain that implementing an efficient evaluator for Colored Petri-nets is in general difficult. Later on this might pose some problems when testing verifying certain requirements.

Petri-nets can be implemented on control-flow machines, that is, machines with a 'fetch', 'execute', 'store', architecture. To do so one needs to keep a marking in working memory. With every time-step this marking is used to verify which transitions are enabled. The current marking in the working memory is then replaced by the new marking.^3.1 However fast in execution, a typical control flow machine suffers from one bottleneck: the memory access: since every single Petri-net step has to fetch and store data in the main working memory, Petri-nets are difficult to map efficiently to commonly used hardware.

Nevertheless, in the past, data-flow machines have been built which are much more efficient in executing Petri-nets. A data-flow machine consists of a number of registers that hold tokens; a token is transferred from operation to operation. In a typical data-flow machine an operation has at most two input-registers and at most two output operations. The input registers are filled in by other instructions that want to pass a token to this operation. The destination registers contain the addresses where to put the result in. These addresses refer to the input registers of other operations. Every operation has also two signaling registers which are used to schedule the passing of tokens. [Moo96] contains a description of a number of existing data-flow machines. Not so strangely the evolution of data-flow machines follows very closely the evolution of formal Petri-net models.

Implementing an evaluator for colored Petri-nets seems trivial: instead of checking whether a token is present and moving the token from the input places to the output places we also have to check a guard. Unfortunately it isn't that simple. Remember the formula 3.2, if we want to know which transitions are enabled we must be able to evaluate the right hand side of that expression. This means that we must find a binding for which the guard (and accompanying expressions) is satisfied. In contrast to an elementary net where we simply have to check whether a token is present we now have to find out which combination of tokens is suitable to satisfy the guard. Fortunately, when searching a suitable combination we only need to take into account the set of all tokens present in places local to the transition under investigation. This means that we don't have to check combinations of tokens in places which are not immediately linked to the current transition. This can be easily seen if we look at the two expressions within formula 3.2. The first requirement, (there should be a $b\in B(t)$), does not necessarily guarantee that the values are present in the places local to $t$. In fact nothing indicates where the values have to come from. It only guarantees that there is a binding which satisfies the guard and which binds all necessary values. The second part of the expression on the other hand $\forall (p,t)\in A:E((p,t))\langle b\rangle$ guarantees that all the values necessary to satisfy the guard are present at the incoming places.

In practice this means that, when a transition has $x$ tokens in total over all its input places (this set is called $X)$ and there are $y$ free variables (this set is called $Y)$ we must try out all combinations over X. If there are many tokens this number grows exponentially. Hence we cannot check whether a transition is enabled in $O(1)$ (as can be done with Elementary Nets). A second aspect in evaluating a Petri-net is knowing which transitions have a chance to be enabled. If we start with an initial marking $M_{0}$ we know that we only have to check the transitions immediately bound to the places containing tokens. So we only need to check out $M_{0}^{\bullet}$. If a certain transition is selected to be executed we need to change the marking from $M_{0}$ to $M_{1}$ as specified in formula 3.3. In human terms this equation transfers a certain number of tokens from the input place(s) to the output place(s), thereby changing the local states of all the input places and all the output places, formally changing the state of $^{\bullet}t\cup t^{\bullet}$. The transitions connected to these places: $(^{\bullet}t\cup t^{\bullet})^{\bullet}$ are the only ones who can possible change from disabled to enabled (or vice versa).

Because of this, it is important to have Petri-nets with enough distinct places: the number of incoming tokens in a transition will likely be smaller if we have more places in a Petri-net. For example, a Petri-net as in figure 3.3 is very small, with only one place. Given the fact that the net is conservative^3.2 and that we start with 3072 tokens, and there are 5 possible enabled transitions, we need to check out 15360 possibilities. This number rises exponentially with the number of input tokens taken by one transition. In comparison, consider the Petri-net in figure 3.2, we start with a token count of 1024 at place LockCount. There are 3 possible output places so we need to check 3072 combinations.

Given the fact that we need to try out all combinations of incoming tokens we might start thinking of using something like a logic engine to evaluate a Petri-net. Indeed, it is very easy to write a Petri-net evaluator in prolog [Fla94]. To do so one simply needs to translate the formal definition of a Petri-net to prolog rules as we will do in chapter 8.

3.5 The Expression Language

THE FORMAL DEFINITION of a colored Petri-net given earlier handled expressions in an abstract way. Therefore we need to define what kind of expressions we will use. The syntax:

$expression\rightarrow unaryexpression \vert binaryexpression \vert compoundexpression \vert atomic$

$compoundexpression\rightarrow '(' operator expression^{*} ')'$

$binaryexpression\rightarrow '(' binary expression_{a} expression_{b} ')'$

$unaryexpression\rightarrow '(' unary expression ')'$

$atomic\rightarrow \langle integer\rangle \vert \langle variable\rangle \vert token$

$unary\rightarrow '!'$

$binary\rightarrow '>' \vert '<' \vert '>=' \vert '<=' \vert '='$

$operator\rightarrow '\&' \vert '\vert' \vert '+' \vert '-' \vert '*' \vert '/'$

$token\rightarrow '[' expression^{*} ']'$

Semantically speaking those expressions are straight forward. In the end everything evaluates to either a token or an integer. There are no other values to work with. If a compound statement is found, the arguments are evaluated in applicative order: they are all evaluated recursively, after that the operator is applied to the given values.

• $+$, $*$ respectively adds, multiplies all given arguments.
• $-$, $/$ respectively subtracts, divides all arguments $(-10 20)$ results in $-10$. $(-10 20 30)$ results in $-40$. $(/16 2 2)$ results in $4$.
• $\&$, $\vert$, $!$ are logic operations. Something is considered to be true if it is not zero.
• $<,>,\leq,\geq,=$are comparison operators. They are not defined on tokens.

As can be seen, there is no way to store variables, everything is functional. The result of an expression is always the same if the input is the same. No side effects can be specified. The fact that we only work with integers is to reduce the complexity of testing our adaptor. Technically it is not difficult to add other types such as strings, floats, structures and others. The only drawback in doing so is that the implementation of the evaluator becomes much larger and we need to add a substantial amount of type checking.

We now define the $Vars$ operator on expressions.

$$Vars( '(' operator term_{0} \ldots term_{n} ')' ):=\bigcup_{term=0}^{n}Vars(term_{i})$$

$$Vars( '[' term_{0} \ldots term_{n} ']' ):=\bigcup_{term=0}^{n}Vars(term_{i})$$

$$Vars( \langle integer\rangle ):=\phi$$

$$Vars( \langle variable\rangle ):=\{ variable\}$$

The $Type$ operator on expressions is defined as

$$Type( '[' term_{0} \ldots term_{n} ']' ):=Type(term_{0})\times\ldots\times Type(term_{n})$$

$$Type( '(' operator term_{0} \ldots term_{n} ')' ):=Type(operator)$$

$$Type( boolean ):=\{0,1\}$$

$$Type( arithmetic ):=Type( \langle integer\rangle ... ...ype( \langle variable\rangle ):=\{\ldots -1,0,1,\ldots\}$$

with $boolean$ either $<,>,\leq,\geq =,\&,\vert,!$ and arithmetic one of $+,-,*,/$. Because all operators work on integers the values assigned to variables can only be integers.

3.6 The Language used to Express Petri-Nets

3.6.1 The Basic Language

WE ARE ABOUT TO USE COLORED PETRI-NETS to describe the behavior of a component. Since a) programmers are supposed to write these and b) our adaptor generation software needs the ability to read and understand them we need a text format to write Petri-nets down in a clear and understandable way, hence:

• There should be no redundancy.
• Every piece of information that can be inferred should be inferred. This is important because it allows us later on to generate Petri-nets that will have those missing pieces deduced instead of reported as inconsistent.
• Things should be written down at the position where people think of them.
• The format should be easy extensible.

We looked at a number of existing Petri-net formats, such as the 'Abstract Petri-net Notation' [FKK95], the Pep internal Petri-net format [BG98], and others but none of them suited our needs, either because they were too verbose or because the format was clearly intended for internal use. For instance a number of Petri-net formats describe the incoming and outgoing arcs at different places from the transition connected to them.

Therefore, we came up with the following basic Petri-net syntax. We also implemented a prototype of a Petri-net evaluator based on this syntax in Java. The Petri-nets are based on the expression syntax given earlier.

$petrinet\rightarrow statement$

$statement\rightarrow$ (place $variable$ $[token]$)

$statement\rightarrow$ (transition $variable$ $inputarcs$ $[outputarcs]$ $[guard]$)

$inputarcs\rightarrow$ (input $(variable [token])^{+}$)

$outputarcs\rightarrow$ (output $(variable [token])^{+}$)

$guard\rightarrow$ (guard $(expression)^{+}$)

With this notation it is easy to write down Petri-net of figure 3.2.

(place LockCount [0..31, 0..31, 0])

(place Locking)

(place UnLocking)

(place Acting)

(transition Lock

  (input LockCount[X,Y,C])

  (output Locking [X,Y,C]))

(transition Lock_True

  (input Locking[X,Y,C])

  (output LockCount[X,Y,C+1]))

(transition Lock_False

  (input Lock_False[X,Y,C])

  (output LockCount[X,Y,C]))

(transition UnLock

  (input LockCount[X,Y,C])

  (output UnLocking[X,Y,C])

  (guard (> C 0)))

(transition UnLock_Done

  (input UnLocking[X,Y,C])

  (output LockCount[X,Y,C-1]))

which is quite readable. Normally, colored Petri-nets have places that describe the type of the tokens that they can hold. In our notation we did not introduce types, because often the type of tokens present at places can be inferred from the type of the expression on the incoming and outgoing arcs to/from transitions. In chapter 8 we will indicate how a type inferencer can be written. We will now investigate how we can extend this notation to be more suitable in an adaptor generation context.

3.6.2 Linking Components $\leftrightarrow$ Petri-Nets

Before we can actually use Petri-nets in an execution environment our Petri-nets need to be linked to this environment. Commonly, Petri-nets have a provision for this under the form of sources and sinks. A source is a place where 'out of the blue' tokens can arrive without prior notification. A sink is a place where the Petri-net can place a token and this token will be automatically removed to perform some action.

Informally a source-place is a place for which there are no incoming arcs. A sink place is a place for which there are no outgoing arcs. Formally this can be written down as

$$p \textrm{is} source \Rightarrow \not\exists t\in T : (t,p)\in A$$

Similarly,

$$p \textrm{is} sink \Rightarrow \not\exists t\in T : (p,t)\in A$$

However, sources and sinks are not only defined based on their presence in the Petri-net. They also have an external behavior associated with them, which is often not expressed within the Petri-net. Below we will define a suitable behavior for sources and sinks such that it can be used within an event based framework.

3.6.2.1 Integration of Messages

The component framework outlined earlier (chapter 2) describes how ports and components can be used to write adaptors easily. The main idea behind the framework is that messages should be the only way to communicate events between components. Therefore it is a logical extension to link every message to a token. Converting messages to tokens and vice versa is done by a set of conversion rules. Every rule describes what a message looks like and declares how the token should be created. Syntactically we define this,

$message\rightarrow$ (message $\langle string\rangle$ $field^{*}$)

$field\rightarrow$ (field $\langle string\rangle$ $expression$)

Converting a message to a token, given a set of such message rules, is done by retrieving all of the unbound variables, sorting them alphabetically and placing them inside a token. For instance

(message LockTrue 

  (field ``X'' X)

  (field ``Y'' Y)

  (field ``Result'' 1))

Figure 3.5: An illustration how sources and sinks can be used to interface a Petri-net with a component.

will match any incoming LockTrue message and convert it to a token $[X,Y]$. The known Result field will not be stored in the token because it is not an unbound variable. For example,
LockTrue(12,15,1) will be matched by the above rule an will result in a token [12,15]. The LockTrue(16,18,0) will not be matched by the above rule, and as such, not generate a token. Likewise, when a token is converted to a message, given a certain message-rule, we simply replace every free variable in the message by the value at the corresponding position within the token.

These message rules give us a means to convert messages to and from tokens. This is necessary to be able to interface a Petri-net with our external component framework. The only thing we still need to define is the way sources and sinks are written down. A source place is a place which generates tokens. In our case, tokens are generated when messages arrive, therefore a source place is described by means of a string (the name), an integer which specified over which port the messages comes from and a message template. Sink places are specified in a similar way.

$statement\rightarrow$ (source $variable$ $\langle integer\rangle$ $message$)

$statement\rightarrow$ (sink $variable$ $\langle integer\rangle$ $message$)

The extra $\langle integer\rangle$ field is necessary for sources to specify the port over which the message comes. For sinks it is necessary to specify the port to which the message should go to. Figure 3.5 illustrates how sources (left side, ending on -in) and sinks (right side, ending on -out) can be used to specify a required message interaction between components.

3.6.2.2 Two Uses for Sources and Sinks

Because this kind of Petri-nets (with sources and sinks) quickly becomes very large, it is impractical to request from the developer to write down all sources and sinks and link them together. However, there are two more reasons why a developer should not write the sources and sinks explicitly down.

1. First, because depending on whether the interface is required or provided the sources and sinks switch places and the Petri-net would need to be rewritten.
2. Secondly, because the sources and sinks can be used to interface a Petri-net between two components, hence link two components together, but they can also be used to link a component to another part of an adaptor.

The second usage will be explained in more detail, after we introduce how in-out transitions are used to describe the linkage with the underlying component.

3.6.3 In/Out Transitions

Figure 3.6: A verification adaptor based on 1 Petri-net offered by either server or client.

Figure 3.7: An adapting adaptor based on 2 Petri-nets offered by client and server.

One of the ideas behind the component framework is that one needs the ability to specify the inverse of an interface. To illustrate this think of a server that offers a locking strategy and a client that expects a locking strategy. The server will specify an incoming Lock message and outgoing LockTrue and LockFalse messages. The client on the other hand will specify exactly the contrary: Lock messages go out and LockTrue or LockFalse messages come in. This can be seen in figure 3.6 and 3.7. The red interface boxes (left) are the ones going toward the server, the blue interface boxes (right) are the ones coming from the client. In practice, the colored transitions are replaced by sources and sinks to match certain messages. The translation from such an incoming or outgoing transition to source and sink places is however not always the same because multiple reasons exist to create such an adaptor.

The first situation is one in which an adaptor traces the behavior of an interaction, without adapting anything. This is useful to test the correct working of both components and the Petri-net specification of the interface. Using such an adaptor ensures that the formal description is in tune with the implementation of the component.

A second situation occurs when an adaptor is required to adapt the behavior of two interfaces. In such a situation there will be two Petri-nets available: one accepting messages from the client and one accepting messages from the server. Both Petri-nets and some 'adaption' logic will reside in the adaptor.

These two cases offer some problems because the behavior of the Petri-net transitions is different. To understand this look at the required behavior of the red and blue lines connected to the transitions. Depending on the situation a transition should behave different

1. In the first case, (figure 3.6), a red transition is enabled only if a certain incoming message arrives (e.g. Lock) over the left port and when triggered a message is immediately sent out to the right port.
2. In the second case, (figure 3.7), there are two different behaviors of the red transitions and blue transitions
   1. the Petri-net tracing the left port will only enable red transitions when a certain message has arrived on the left port. If such a red transition is executed the adaptor is informed. The blue transitions on the left are only executed when the adaptor logic requests so. In response they will send out a certain message to the left port.
   2. the Petri-net tracing the right port will only enable blue transitions when a certain message has arrived on the right port. If such a blue transition is executed the adaptor is informed. The red transitions on the right are only executed when the adaptor requests so. In response they will send out a certain message to the right port.

As can be seen, the actual Petri-nets generated out of interface Petri-net descriptions might need to do completely different things. Therefore we extended the basic Petri-net syntax with two extra transition types: in-transitions and out-transitions. From the point of view of a component an in-transition describes a message that arrives for the component, an out-transition describes a possible message that can be send out. Since both transitions have to handle incoming or outgoing messages they take some extra arguments.

The extended Petri-net notation:

$statement\rightarrow$ (intransition $variable$ $inputarcs$ $[outputarcs]$ $[guard]$ $message$)

$statement\rightarrow$ (outtransition $variable$ $inputarcs$ $[outputarcs]$ $[guard]$ $message$)

In order to be able to transform the in-transitions and out-transitions to an executable Petri-net we have added special source and sink places (as is done in almost all Petri-net tools). In figures 3.8 and 3.9, the source places are colored green and will contain a token when a message arrives, the sink places are colored red and the underlying component will sent out a message when a token arrives at those places.

Figure 3.8: Conversion of an in-transition/out-transition to standard sources, sinks and transitions when interpreted as a tracing adaptor.

Transforming a Petri-net to be used in a tracing Petri-net adaptor (illustrated in figure 3.8):

• (intransition $variable$ $inputarcs$ $outputarcs$ $guard$ $message$) is replaced by
  (source $variable$-in 0 $message$)
  (sink $variable$-out 1 $message$)
  (transition $variable$ $inputarcs\cup variable$-in $outputarcs\cup variable$-out $guard$)
• (outtransition $variable$ $inputarcs$ $outputarcs$ $guard$ $message$) is replaced by
  (source $variable$-in 1 $message$)
  (sink $variable$-out 0 $message$)
  (transition $variable$ $inputarcs\cup variable$-in $outputarcs\cup variable$-out $guard$)

Figure 3.9: Conversion of an in/out transition to sources, sinks, places and transitions when interpreted as an adaptor.

Transforming a Petri-net to be used in an adaptor (illustrated in figure 3.9), requires another transformation logic for the in/out transitions; For the left port this becomes

• (intransition $variable$ $inputarcs$ $outputarcs$ $guard$ $message$) is replaced by
  (source $variable$-in 0 $message$)
  (place $variable$-out)
  (transition $variable$ $inputarcs\cup variable$-in $outputarcs\cup variable$-out $guard$)
• (outtransition $variable$ $inputarcs$ $outputarcs$ $guard$ $message$) is replaced by
  (place $variable$-in 0)
  (sink $variable$-out 0 $message$)
  (transition $variable$ $inputarcs\cup variable$-in $outputarcs\cup variable$-out $guard$)

For the right port this becomes:

• (intransition $variable$ $inputarcs$ $outputarcs$ $guard$ $message$) is replaced by
  (source $variable$-in 1 $message$)
  (place $variable$-out)
  (transition $variable$ $inputarcs\cup variable$-in $outputarcs\cup variable$-out $guard$)
• (outtransition $variable$ $inputarcs$ $outputarcs$ $guard$ $message$) is replaced by
  (place $variable$-in 1)
  (sink $variable$-out 1 $message$)
  (transition $variable$ $inputarcs\cup variable$-in $outputarcs\cup variable$-out $guard$)

By using these in-transitions and out-transitions we have

• increased the readability of interface description. Instead of needing to express all input/output places and a transition we now simply write one statement.
• increased the flexibility of using these transitions within tools. We can either use the Petri-nets as a tracing adaptor or in combination with another Petri-net as an adaptor.

3.7 Two More Complex Examples

IN THIS SECTION WE GIVE TWO examples of more difficult locking interfaces that can be expressed by means of Petri-nets. The first example covers a layered concurrency strategy. The second covers a rollback-able concurrency strategy.

3.7.1 Interface Description of a Blocking Layered Concurrency Strategy

Figure 3.10: A Layered Concurrency Strategy expressed as a Petri-net

Figure 3.10 contains an example of a layered concurrency strategy that works in different stages. This example demonstrates how well suited Petri-nets can be to describe subtle interaction patterns between different 'modes' of an interface. The concurrency interface itself describes a) the behavior that can be executed upon certain resources and b) the synchronization behavior that need to be used before these resources are accessible. The concurrency strategy is layered. This means that, before the actual resources can be locked, the server needs to be locked entirely by the client. Once all the locks are obtained the server itself can be released, such that other component might start a set of locking operations. This example has a number of interesting features

• It shows how synchronous calls can be written down. This is visualized in the light blue box. The Petri-net starts in the start place. Before any whiteboard action (isfree, set_position) can be executed, the joinactor message must be sent. When this has been done, the Petri-net puts a token in the waiting_join place. The token that was originally present in the start place is no longer there, which means that a joinactor message cannot be received anymore. Once the return_join message has been sent, the Petri-net will put a token in the ready place, which enables all further whiteboard actions in the Petri-net.
• It shows how different modules can be put together. In this example, two synchronization systems are in place. The first offering a server lock (the light green box). The second offering a locking strategy that allows to lock positions on the whiteboard (the light yellow box). The interaction between these two modules is minimal. Only when the server is locked, then can a position be locked (the arrow going from the entered place to the lock transition).
• It shows how subtle interactions between modules can be expressed. For instance,
  • it is not possible to handle a second lock request as long as the first has not yet been handled entirely (a lock_done is send back). In the Petri-net this is expressed by two arcs. The first one pulls a token from the entered place and does not put it back. The second one will put it back when the lock_done message is sent.
  • Contrary to the locking operation, the unlock operation can be executed without a server lock.
  • when a position is locked and the server is not locked then it is possible to access the whiteboard with the set_position and is_free operations, because both operations only depends on the locked place and not on the entered place.
• It shows on multiple occasions how synchronous calls can be expressed. The places ready and busy are used by all whiteboard actions (set_position, is_free, return_free_true, return_free_false and return_set_position). Both places ensure that no new operation will be handled as long as the current operation is not yet entirely processed.
• This example also shows a Petri-net with multiple tokens per place. When initialized, the start and not_entered place contains a token. Similarly, the locked place will be initialized with zero-locks for every available position.

3.7.2 Description of a Non-blocking Rollback-able Concurrency Strategy

Figure 3.11: A rollback-able concurrency strategy.

The example given in figure 3.11 shows how a concurrency strategy that makes use of rollbacks can be written down. Locks can be requested, when they are granted they can be either committed or aborted. If a lock is aborted the previous state will be recalled, if a lock is committed the previous state is forgotten. Important features of this Petri-net are:

• The square place keeps track of the current state of the whiteboard as well as all previous states that it needs to remember. This is done by coupling to every position a color (content of that position) and a version. The type of this place is [X Y Content Version]. The current version is the latest version an can be found by looking at the current lock-count. The lock counts are stored in the lock place.
• The abort operation works by pulling the current version of a certain position and decreasing the lock counter.
• The commit operation works by pulling a) the current version and b) the previous version of certain place. The content of the current state is put back with the old version number. The lock counter is decreased by one.
• The Petri-net itself is unbounded. This means that, at runtime, the amount of tokens can be infinite. For every acknowledged lock, the square place will receive one token extra. Because there is no limit on how many locks can be requested, the Petri-net is unbounded.
• The Petri-net describes an interface that works non blocking. Locks can be queued and handled one by one by the underlying component. If there is no required order upon the message-handling this might lead to disastrous results. For instance, suppose a client has locked 5 times the same position and request two abort and 3 commits. Depending on the order in which the commits and aborts are handled completely different results might occur. Later on we will require that the Petri-net finishes executing before a new message can be handled. This is necessary to avoid this kind of problems.

3.8 The Do-Not 's of Interface Petri-Net Descriptions

PETRI-NETS ALLOW THE PROGRAMMER of a component to document the required and provided interfaces of a component. Nevertheless there are some issues which should be taken into account. Not every Petri-net expresses as much as another Petri-net. For instance, one Petri-net of a component might specify that every incoming message can be handled at any time, while another Petri-net will carefully offer pre-conditions and postconditions for this message to be handled. To help the programmer write down Petri-nets that make sense we introduce some guide rules to write them:

• A Petri-net interface description should always be fully connected. If we take the transitive closure over any transition or place we should end up with the entire Petri-net.^3.3 This is important because otherwise we would have a set of unrelated message-handlers. A Petri-net such as: if message a comes in, then message a goes out, if message b comes in, then message b goes out does not say much more than what a simple syntactical description also says.
• There should be no places, other than sink-places, which have no outgoing arcs. Such places introduce some extra information in the Petri-net that can never be used because it is not related to anything else.
• In the Petri-net notation introduced in this chapter we never explicitly mention the type of a place, nevertheless the type of tokens that can arrive at a place should be consistent (= the same for every possible transition). Chapter 8.3 contains material that allows one to infer the types within a Petri-net.
• All possible incoming an outgoing messages of a component should be documented in the Petri-net description. It is to be avoided at all times to specify only part of an interface. To guarantee this a tracing adaptor is very useful.
• A Petri-net description of an interface should be as specific as possible. It should leave as few transitions enabled as possible. For instance, it is always possible to indicate that a message can be handled at any time and return an error when somebody sends this message. This can be described in an interface, but if it is not part of the behavior of the interface it should not be written down. Instead one should write down a Petri-net that clearly disables this transition when the associated action doesn't make sense.
• When a message arrives at a Petri-net, at most 1 place should be able to accept the message. With the Petri-net notation described in this chapter it is possible to write a transition which reacts to a message of the type (message (field ``X'' 1) (field ``Y'' Y)), and another transition that reacts to (message (field ``X'' X) (field ``Y'' 1)). When a message (1,1) arrives, both transitions will be enabled at once. However, this should not be allowed. With the material in chapter 8.3 it will be possible to check these kind of constraints automatically. However, we will not focus on them anymore.

3.9 Defining Conflicts

By means of Petri-nets we will be able to define clearly what a conflict is. Therefore we will rely on the existence of a certain link between two Petri-nets. This link will consist of the common transitions and will be called the functional link. All the other transitions within a Petri-net will be considered to be part of the synchronization interface.

We will also assume that both Petri-nets are linked in such a way that the firing of one transition is mapped onto the firing of a similar transition in the other Petri-net (this can be accomplished by inserting an adaptor or by hardwiring the transitions by means of inserting common places, as we've done in section 3.6.3). For instance, when a SetPosition message arrives, then the first Petri-net will fire a SetPosition. Afterward, the second Petri-net (of the outgoing link) also needs to fire a SetPosition, otherwise no communication will occur between both components.

If the Petri-nets are used as such, then we can define a conflict as a situation in which an incoming functional message $m$ can be accepted by the first Petri-net, but not by the second Petri-net because the required preconditions does not hold. E.g, an incoming setPosition that cannot be execute on the server because the position is not locked yet (this will be described within the server side Petri-net and will form the blocking pre-condition of the SetPosition transition).

Formally, two Petri-nets $N_{0}$ and $N_{1}$ are, given two markings $M_{0}$ and $M_{1}$, in conflict when a logic transition exists that is enabled in only one of both interfaces. We will use $\not\approx$ to denote a conflict between two Petri-net markings:

$$(N_{0},M_{0})\not\approx(N_{1},M_{1}) \Leftrightarrow \exi... ...c, \vert M_{0}[t\rangle_{N_{0}}\wedge M_{1}[t\rangle_{N_{1}}$$ (3.4)

3.10 A Word on Formal Analysis of Petri-Nets

BELOW WE WILL INTRODUCE a number of formal properties of Petri-nets. Not all of them are decidable.

• Boundedness: A Petri-net is bounded if the set of all possible markings generated by a petri-net is finite. This property is decidable, it is even possible to check whether the maximum number of tokens arriving at one place doesn't become larger than $k$. In this case a petri-net is called $k-$bounded. In our situation, we can not always talk about boundedness because the Petri-net descriptions of an interface contains source places that can fire at any moment, so the number of tokens is essentially unknown.
• Reachability: A marking $M$ is reachable from marking $M_{0}$ under Petri-net $N$ if there exists a sequence of transitions leading from $M_{0}$ to $M$: $M_{0}[t_{0}\rangle M_{1}[t_{1}\rangle\ldots M$. This is a very important property because it allows us to decide whether a certain error condition can be met or not. Recursively we can define this as follows:

$$M \textrm{reachable under} N \textrm{from} M_{0} \iff$$

$$M=M_{0}\vee\exists M'\in{}^{\bullet\bullet}M \vert M' \textrm{reachable under} N \textrm{from} M_{0}$$ (3.5)

This property is decidable and forms the basis for many other properties. In chapter 8 we will explain in more detail how this kind of information can be obtained.

• Deadlock-freedom: A Petri-net is deadlock free if every reachable marking enables some transition. This property is decidable because it can be reduced to the reachability problem. This definition will later on give rise to our notion of application deadlocks within our event based system. (section 5.2)
• Liveness: A Petri-net is alive if every transition can always occur again. Whether this is decidable or not is still an open question. This will turn out to be an important property, because it tells us that a certain concurrency strategy does not lock out certain functional behavior. For bounded Petri-nets it is known that liveness is decidable because it reduces to reachability. However, because we cannot always rely on boundedness because our Petri-net can receive a token at any moment, we must assume that this property is undecidable.
• Homestate-problem: A Petri-net has a home state $M$ if this marking can be reached from every other marking. The question to decide now is whether a given marking is a homestate for a certain Petri-net. This problem has been shown to be decidable.
• Non-Termination: The question whether a Petri-net will never terminate is undecidable.

For a survey on the decidability of Petri-nets see [EN94]. All the above properties are valid on elementary nets and certain colored petri-nets, depending on the expression language chosen within the colored net. However, a lot of petri-net variants exist which somehow introduce a check for the absence of a token. In such Petri-nets a transition can be enabled if there is no token at a certain place. If such a construction is added to a Petri-net one loses all decidability as is shown in chapter 7 of [Pet81].

3.11 Summary

IN ORDER FOR AN ADAPTOR to mediate the behavior of two conflicting interfaces, it needs extra formal documentation. The formalism we will use to represent the behavior of an interface are Petri-nets because it allows us to

• Express interfaces in a natural way.
• Express an interface up to a chosen level of detail, but still complete.
• Simulate the behavior of an interface without actually having the implementation of the interface at hand.

After having introduced Petri-nets we explained the link between Petri-nets and the event based model of chapter 2. This is done by means of in- and out- transitions. Depending on the situation we can translate these special transitions to other Petri-nets. We gave two examples of this: a tracing Petri-net adaptor between interfaces which are known to work together and an adaptor between two different interfaces. We also gave an overview of possible formal analysis that can be carried out on Petri-nets.

We wrapped up this chapter with giving some guidelines to the developer to write Petri-nets and gave a short introduction to which properties are decidable for Petri-nets.

The Petri-nets we have described here will be used further on for two purposes:

1. Describe the behavior of the components in an understandable and useful way.
2. Describe the behavior of a liveness module.

Before we do so, we will focus on the last of the preliminaries: learning algorithms.

Footnotes

...^3.1

Instead of testing all transitions to a certain marking it would be more useful to check only all postconditions of a marking.

... conservative^3.2

A Petri-net is said to be conservative if the total number of tokens present doesn't change over time.

...^3.3

The transitive closure does not take the direction of arrows into account.