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.

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. 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. 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: 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. 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. 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'. 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]. 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. 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:

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:

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:

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

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\}\}$

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 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)\end{displaymath}

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)
\end{displaymath} (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)
\end{displaymath} (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\}\end{displaymath}

$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
\end{displaymath} (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\}\end{displaymath}

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\}\end{displaymath}

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

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 conservative3.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.

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})\end{displaymath}

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

Vars(  \langle integer\rangle  ):=\phi\end{displaymath}

Vars(  \langle variable\rangle  ):=\{ variable\}\end{displaymath}

The $Type$ operator on expressions is defined as

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

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

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

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

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:

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\end{displaymath}


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

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. 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. 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):

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

For the right port this becomes:

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

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

% latex2html id marker 1622
...tri-net description of a blocking layered concurrency strategy.}

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

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

Figure 3.11: A rollback-able concurrency strategy.

% latex2html id marker 2057
\setle... describing non-blocking 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:

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:

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}}\end{displaymath} (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.

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

M=M_{0}\vee\exists M'\in{}^{\bullet\bullet}M \vert  M' \textrm{reachable under}  N \textrm{from}  M_{0}
\end{displaymath} (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.

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

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.


Instead of testing all transitions to a certain marking it would be more useful to check only all postconditions of a marking.
... conservative3.2
A Petri-net is said to be conservative if the total number of tokens present doesn't change over time.
The transitive closure does not take the direction of arrows into account.
Werner 2004-03-07