O'Reilly logo

Verification of Communication Protocols in Web Services: Model-Checking Service Compositions by Peter Bertok, Zahir Tari, Kazi Sakib

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required