Structural model checking

The introduction of symbolic approaches, based on Binary Decision Diagrams (BDD), to Model Checking has led to significant improvements in Formal Verification, by allowing the analysis of very large systems, such as complex circuit designs. These were previously beyond the reach of traditional, explicit methods, due to the state space explosion phenomenon. However, after the initial success, the BDD technology has peaked, due to a similar problem, the BDD explosion.;We present a new approach to symbolic Model Checking that is based on exploiting the system structure. This technique is characterized by several unique features, including an encoding of states with Multiway Decision Diagrams (MDD) and of transitions with boolean Kronecker matrices. This approach naturally captures the property of event locality, inherently present in the class of globally asynchronous/locally synchronous systems.;The most important contribution of our work is the saturation algorithm for state space construction. Using saturation, the peak size of the MDD (luring the exploration is drastically reduced, often to sizes equal or comparable to the final MDD size, which makes it optimal in these terms. Subsequently, saturation can achieve similar reductions in runtimes. When compared to the leading state-of-the art tools based on traditional symbolic approaches, saturation is up to 100,000 times faster and uses up to 1,000 times less memory. This enables our approach to study much larger systems than ever considered. Following the success in state space exploration, we extend the applicability of the saturation algorithm to CTL Model Checking, and also to efficient generation of shortest length counterexamples for safety properties, with similar results.;This approach to automatic verification is implemented in the tool SMART. We test the new model checker on a real life, industrial size application: the NASA Runway Safety Monitor (RSM). The analysis exposes a number of potential problems with the decision procedure designed to signal all hazardous situations during takeoff and landing procedures on runways. Attempts to verify RSM with other model checkers (NuSMV, SPIN) fail due to excessive memory consumption, showing that our structural method is superior to existing symbolic approaches