Verification of Communication Protocols in Web Services: Model-Checking Service Compositions

CHAPTER 3

PETRI NETS

As discussed in Chapter 2, model checking necessitates a formal representation of a system prior to verifying it. Essentially, this involves creating a formal model of the system using any of the modeling languages available (e.g., Promela, petrinets, a process algebra, an automaton) [3]. However, the modeling language used significantly influences the properties of the model rendered. For example, the concurrent constructs of a system cannot be mapped into its model using an automaton.

A petri net (PN) is a mathematical modeling language and a graphical tool for the description and analysis of concurrent, asynchronous, parallel, distributed, nondeterministic, and stochastic systems [12]. As a graphical tool, it offers elements to create the formal representation of a system. Then mathematical analysis techniques can be used to render the behavior and properties of the system represented. Such analysis usually involves a computer-based tool for automation.

Petri nets are directed bipartite graphs that consist of places (circles) and transitions (rectangles) connected by arcs. The tokens (black dots) in the places define the state of a petri net. Events associated with a transition move the tokens between adjoining places along the arcs. Petri nets have been widely used as a design language for the specification of intricate workflows [16], owing to their graphical nature, expressiveness, formal semantics, and analysis techniques.

FIGURE 3.1 Petri net model ...