文档介绍：SE-561 Formal Methods in Software s - I
s
The classical was invented by Carl Adam Petri in 1962.
A lot of research has been conducted (>10,000 publications).
Until 1985 it was mainly used by theoreticians.
Since the 80-ties the practical use is increasing because of the introduction of high-level s and the availability of many tools.
High-level s are s extended with
color (for the modeling of attributes)
time (for performance analysis)
hierarchy (for the structuring of models)
The classical model
A is posed of places ( ) and transitions ( ).
t2
p1
p2
p3
p4
t3
t1
Connections, called arcs, are directed and between a place and a transition.
Tokens ( ) are the dynamic objects.
The state of a , called marking, is determined by the distribution of tokens over the places.
Initial marking (1, 2, 0, 0)
Transition t1 has three input places (p1, p2 and p3) and two output places (p3 and p4).
Place p3 is both an input and an output place of t1.
p1
p2
p3
p4
t1
Enabling condition
Transitions are the ponents, while places and tokens are passive.
A transition is enabled if each of the input places contains tokens.
t1
t2
Transition t1 is not enabled, transition t2 is enabled.
Firing
An enabled transition may fire.
Firing corresponds to consuming tokens from the input places and producing tokens for the output places.
t2
t2
Firing is atomic.
Example
Structures
sequence of events/actions:
concurrent execution:
t1
t2
t3
t1
t2
t3
t4
t5
Non-determinism
Two transitions fight for the same token: conflict.
Even if there are two tokens, there is still a conflict.
t1
t2
t1
Synchronization
Modeling
States of a process or a system are modeled by tokens in places and state transitions leading from one state to another are modeled by transitions.
Tokens represent objects (humans, goods, machines), information, conditions or states of objects.
Places represent buffers, channels, geographical locations, conditions or states.
Transitions represe