SOFTWARE DESIGN VERIFICATION AND VALIDATION - Software Design for Six-Sigma: A Roadmap for Excellence - page 511

TABLE 19.1 Relation between Petri Net and Business Process

Petri Net Process Model

Store-place Resources (like employees, warehouse), resource state (like busy idle) process

Transition Beginning or ending of operation, events, process and time

Token Resource, resource amount

Label System state

Accessibility Whether system can reach certain state

Table 19.1 shows the relation between Petri Net and business process.
In the Petri Net flow diagram, we usually have a preference relation, parallel
relation, conditional branch relation, circular relation, and other basic relations.

19.4.3.1.1 Process Knowledge Verification Technologies Based on Petri
Net. A process model is the result of a business process design. Thus, its con-
struction is a complex process. In a system, business models of different enterprises
are mapped to the Petri Net model according to the interface technology, then relative
data output, and finally the process model is verified according to relevant theories
and methods.
A good summary that summarized the properties needed to be verified in process
model verification is Commoner's Deadlocks in Petri Nets (1972). The basic prop-
erties of Petri Net are classified into two major kinds: one is dynamic properties that
depend on initial marking, such as accessibility, boundedness, reliability, activity,
coverability, continuity, fairness, and so on; the other is structure properties that do
not depend on initial marking, such as structural liveness, repeatability, and consis-
tency. The mentioned properties all are consistent with basic properties of Petri Net,
and Petri Net has remarkable advantages in process model verification. Reachability
is the most basic dynamic properties of Petri Net, and the rest of the properties can
be defined by it. However, Boundedness reflects the demand for resource volumes
while the system is running.

19.4.3.1.2 Deadlock Issue. If transition from state A to state B is impossible
(directly or indirectly), then the transition is said to be unreachable. If it is unreachable
from the initial state to a certain state, then it demonstrates that there are mistakes in
the workflow (Girault & Valk, 2003).
All entities in a process are in a waiting state. The entities can change its state when
an event occurs. If this certain event is impossible in the state, then it state is called
a deadlock state. The other form of deadlock that can occur in the system is caused
by an endless loop that no other events can help get rid of. This kind of deadlock is
called livelock, which means that the overall state is changing, but it cannot get rid
of the dead circle.
There are many analysis methods used with Petri Nets, among them are the
reachability tree (Kovalyov et al., 2000), coverability trees, and incidence matrices
with state equation.