Information Technology Reference
In-Depth Information
resources in the transition process. The second row shows that the model is safe,
which indicates that the token number of all places in the model is no more than one
token. The third row shows that there is no deadlock in the model, which shows that
deadlock is impossible for resource competition.
19.4.3.1.4 EvaluatingVerificationapproachusingPetriNet.
When using Petri
Nets, a process model gains some effective verification methods. It ensures the
correctness and effectiveness of the process model. This method provides practica
and effective means for the management and maintenance of the domain knowledge
system.
19.4.4
A Hybrid Verification Approach
Hybrid verification technology, which has been tested on current Intel designs, com-
bines symbolic trajectory evaluation (STE) with either symbolic model checking
(SMC) or SAT
11
-based model checking. Both human and computing costs are re-
duced by this hybrid approach.
STE deals with much larger circuits than SMC. It computes characteristic or
parametric representation sequence of states as initial values (Hazelhurst, 2002) and
then executes the circuit and checks to see that the consequent is satisfied. STE com-
plements SMC, in which SMC is one of the more automated techniques but requires
human intervention in modeling. It deals more with commercial sequential designs,
and it is limited with respect to the size of verifiable designs (McMillan, 1993).
In the hybrid approach (which we call MIST), the user of the model provides a
design being tested and the specification just as if using a classic model checker.
However, the user specifies the design behavior being tested or the initial state(s) for
the model checker.
The hybrid verification flow consists of two phases:
1. STE performs the initializing computation and calculates the state (or set of
states) that the design would be in at the end of this initialization process.
2. Using the set of states in the previous step as the starting point, a SAT/BDD-
based model checker completes the verification (Hazelhurst & Seger, 1997).
19.4.4.1 Hybrid Method Workflow.
The hybrid approach works as follows
(Hazelhurst et al., 2002):
1. Build
M'
—a pruned model of
M
(automated step). The initializing behavior
and inputs of
M
are given by an STE antecedent,
A
.
2. Use STE to exercise the
unpruned
model
M
under the influence of
A
. STE's
ability to deal with the large unpruned model easily provides the key benefits
of enhancements of performance and simplification of modeling.
11
SATisfiability: Given a propositional formula, find if there exists an assignment to Boolean variables
that makes the formula true.
Search WWH ::
Custom Search