Next: NUSMV: Look and Feel
Up: Symbolic Model Checking
Previous: Symbolic Representation of Kripke
The use of BDDs (i.e. the implicit representation of the transition
system) makes it possible to verify very large systems (larger than
1020 states [12,47,11]). Symbolic model checking has been
successful in various fields, allowing the discovery of design
bugs that were very difficult to highlight with traditional
Some of the most significant results are given below (an extensive discussion
of the applications of symbolic model checking can be found in ):
- in  the authors applied this technique to verify
the cache coherence protocol described in the IEEE Futurebus+
Standard 896.1.1991. They found a number of previously
undetected and potential errors in the design of the protocol.
- in [47,46] the authors verified the cache
consistency protocol developed at Encore Compute Corporation
for their Gigamax distributed multiprocessor.
- in  the cache coherence protocol of the Scalable
Coherent Interface, IEEE Standard 1596-1992 was verified, and
several errors were found.
- in  the authors verified part of a preliminary
version of the system requirement specifications of TCAS II
(Traffic Alert and Collision Avoidance System II). TCAS II is
an aircraft collision avoidance system required on most
commercial aircraft in United States.
- in [18,39] model checking techniques are
used in the verification of a railway interlocking