Introduction
Several tools are grouped under this section. They all provide services
related to the computation of structural properties. The following services
are available now:
Invariants
In many models of parallelism, there are only two methods of validation:
analysis of the accessibility graph or verification of properties from
axioms and inference rules. The first method cannot be used on real systems
since the size of the graph is generally too huge whilst the drawbacks
of the second one are:
- a property may be true even if not provable in the formal system,
- a property may be verified but not computed.
An important advantage of Petri nets over the other models of parallelism
is the existence of alternative and constructive proof methods such as
the flows computation. The flow analysis is an efficient tool for colored
Petri net used in automatic proofs of a systems model. For a parallel
system, the modeller searches two kinds of properties: safeness properties
and liveness properties. For instance, a safeness property could state
that a resource is never shared whilst a liveness property could state
that every user who wants to own this resource will eventually own it.
CPN-AMi may also compute a linear charaterization of the reachability
set. Results are split up into invariants and properties. Invariants can
be used for any initial marking, provided that the constant in the contraints
are modified according to the new initial marking. On the other hand,
properties are (usually) dependant of the initial marking.
Invariant services
CPN-AMI provides various services for the computation of Petri nets invariants:
some of them have been developpedn by our team, some others are imported
from GreatSPN:
a well known software package for the modeling, validation, and performance
evaluation of distributed systems using Generalized Stochastic Petri Nets
designed in the universities of Torino and Genova (Italy).
the following services are available now:
Bounds
Computing places bounds is often used as a first step in a validation
process. It is an important property to check mutual exclusion or the
appropriate use of a set of resources.
Bound services
CPN-AMI is able to compute:
Syphoon and Traps
A Trap (resp. a Deadlock) is a set of places where, for any place in
the set, if a transition can remove (resp. add) tokens from the place,
then this transition add (resp. remove) tokens to another place in the
set. Those properties are thus properties over the structure of the model.
From the definition, a Trap (respectively a Deadlock) cannot be emptied
(resp. filled) when it has been marked (resp. emptied). The tools we present
compute a generative family of Traps and Deadlocks.
One of the implemented algorithm come from GreatSPN.
The other one relies on the use of binary decision diagrams (BDDs) as
data structure. A survey on BDD can be find in [Bryan
92].A use of BDD in the context of Petri net is presented in [Pastor
94]. The BDD based algorithm is faster than the one of GreatSPN.
Both behavior and display of results are very similar to the one of P-invariant,
as shown in the figure below
Example of result for a P/T net.
Liveness for 1-bounded
nets
A net is live if and only if from any reachable state and for any transition
it is possible to reach a state from which the transition is firable.
These services allows to verify the liveness of a safe net (1-bounded).
The verbose mode provides is slower but provides more information when
the property is not verified.
Display of Results
The quiet evaluation of liveness is displayed in the historic window.
In verbose mode, indication are provided if the model is dead: one transition
is outlined in the set of transitions that belong to paths leading to
dead markings. This is shown in the figure below.
Outline of on of the transition that causes a deadlock.
Please note that if the computation is tool long, you can cancel the
execution by clicking on the STOP button in the execution
window.
|
