Fields of Application

The use of BDDs (i.e. the implicit representation of the transition system) makes it possible to verify very large systems (larger than 10²⁰ 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 techniques. Some of the most significant results are given below (an extensive discussion of the applications of symbolic model checking can be found in [27]):

• in [22] 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 [31] the cache coherence protocol of the Scalable Coherent Interface, IEEE Standard 1596-1992 was verified, and several errors were found.
• in [1] 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 system.