SYMBOLIC TECHNIQUES FOR FORMALLY VERIFYING INDUSTRIAL-SYSTEMS

The design of correct computer systems is extremely difficult. However , it is also a very important task. Such systems are frequently used i n applications where failures can have catastrophic consequences, or c ause significant financial losses. Simulation and testing are the most widely used verification techniques, but they can only show the prese nce of errors and cannot demonstrate correctness. Until lately formal methods were too expensive to be used in industrial problems, but rece nt research has made it possible to apply formal techniques to the ver ification of complex real-world systems. Symbolic model checking is an example of such a technique that has been successful in verifying lar ge finite-state systems. It has also been extended to produce timing a nd performance information. These properties are extremely important i n the design of high-performance systems and time-critical application s. A more detailed analysis of a model is possible using these extensi ons than by simply determining whether a property is satisfied or not. We present algorithms that determine the exact bounds on the delay be tween two specified events and the number of occurrences of another ev ent in all such intervals. To demonstrate how our method works, we pre sent two complex examples: the verification of the Futurebus+ cache co herence protocol and the timing analysis of the PCI local bus. These r esults show the usefulness of symbolic model checking in analyzing mod em industrial designs. (C) 1997 Elsevier Science B.V.