Model checking is a method of formal verification that is gaining in popularity as a tool for use in designing complex systems, such as integrated circuits. The method is described generally by Clarke et al. in Model Checking (MIT Press, 1999), which is incorporated herein by reference. To perform model checking of the design of a device, a user reads the definition and functional specifications of the device and then, based on this information, writes a set of properties {φi} (also known as a specification) that the design is expected to fulfill. A model M (also known as an implementation) of the design, which is typically written in a hardware description language, is then verified to ascertain that the model satisfies all of the properties in the set, i.e., ∀φε{φi}, M|=φ, under all possible input sequences. When a property φ is found to be false on M, the model checker returns a sequence of states and transitions (a path) that leads to the problematic state of the design. This path is called a counterexample. It can be used by the engineer in understanding and remedying the design defect that led to the failure of the model.
The properties {φi} for use in model checking are typically written in a suitable specification language for expressing temporal logic relationships between the inputs and outputs of the device. Such languages are commonly based on a temporal logic, such as Computation Tree Logic (CTL) or Linear Temporal Logic (LTL). Model checking can then be carried out automatically by a symbolic model checking program, such as SMV, as described, for example, by McMillan in Symbolic Model Checking (Kluwer Academic Publishers, 1993), which is incorporated herein by reference. Symbolic CTL model checking involves computing the transition-relation (TR) of the model, and then applying the model checking algorithm to verify a given CTL formula.
A number of practical model checking tools are available, among them RuleBase, developed by IBM Corporation. This tool is described by Beer et al. in “RuleBase: an Industry-Oriented Formal Verification Tool,” in Proceedings of the Design Automation Conference DAC'96 (Las Vegas, Nev., 1996), which is incorporated herein by reference. In another article, entitled “On-the-fly Model Checking of RCTL Formulas,” in Proceedings of the Tenth International Conference on Computer Aided Verification (CAV 1998), which is incorporated here in by reference, Beer et al. define a specification language RCTL, as an extension to the conventional CTL language using regular expressions. RCTL makes it possible to translate many CTL formulas conveniently into state machines having an error state. More recently, Beer et al. have extended RCTL to include further expressions and syntax that are useful in creating formulas for model checking, which they describe in “The Temporal Logic Sugar,” Proceedings of the Thirteenth International Conference on Computer Aided Verification (CAV 2001), which is incorporated herein by reference.
Although model checking has gained wide acceptance in hardware design, it is still rarely used in mainstream software development. There are two major reasons for the low penetration of model checking in the software field:    (1) The semantics of software programming languages are difficult to translate into models for existing model checkers. By contrast, fully-automatic tools exist for translating gate-level hardware description languages into a form amenable to model checking.    (2) Software programs generally have an infinite number of states, whereas hardware devices can be treated as finite state systems.The effort to develop new model checkers that address the features of software design is still in its infancy. Such software model checkers are still far from achieving the degree of automation and versatility offered by existing hardware model checkers, such as RuleBase. There is a need for tools that can automatically convert software source code into models that can be handled in a similar way to hardware models, using proven model checking tools.
For this purpose, a number of research groups have developed methods for converting software source code into modeling languages. For example, Demartini et al. describe a method for applying the SPIN model checker to Java programs in “Modeling and Validation of Java Multithreading Applications Using SPIN,” published in Proceedings of the Fourth International SPIN Workshop (Paris, France, 1998), which is incorporated herein by reference. They use a “Java2Spin” translator tool to convert the Java source code into an abstract formal model expressed in the Promela language used by SPIN. Synchronization among threads is modeled using message queues and global variables. The model complexity is kept low by avoiding explicit modeling of library classes, by letting the user specify which variables need to be modeled and by applying other model reduction techniques. A similar approach is described by Havelund et al. in “Model Checking Java Programs Using Java PathFinder,” International Journal for Software Tools for Technology Transfer (Springer Verlag, April, 2000), page 366, which is also incorporated herein by reference.
Holzmann et al. describe another method for automated model generation from software code in “Software Model Checking: Extracting Verification Models from Source Code,” published in Proceedings of PSTV/FORTE99 (Kluwer, 1999), page 481, which is incorporated herein by reference. (PSTV stands for “Protocol Specification, Testing and Verification,” while FORTE stands for “Formal Description Techniques for Distributed Systems and Communication Protocols.”) The authors extract a control-flow skeleton from C language code using a semi-automatic, user-guided procedure, and use a look-up table to convert specific source statements into corresponding Promela modeling code. To produce the final model in Promela, every abstract data object must be formally declared, defining its type and initial value. The user carries out this step by filling in a model template that contains the required data declarations and an outline of the required process declarations. Holzmann describes this method further in “Logic Verification of ANSI-C Code with SPIN,” in Proceedings of the Seventh International SPIN Workshop (Springer Verlag, 2000), page 224, which is also incorporated herein by reference.
Corbett et al. describe yet another tool for automated model generation in “Bandera: Extracting Finite-state Models from Java Source Code,” in Proceedings of the 22nd International Conference on Software Engineering (Limerick, Ireland, June, 2000, published by the Association for Computing Machinery), page 439, which is incorporated herein by reference. Bandera has a number of components, including an abstraction engine, which allows the user to reduce the cardinality of data sets associated with variables. It also provides a language for use in specifying abstractions. Bandera generates a low-level intermediate language based on guarded commands, which abstracts common model checker input languages.
Esparza et al. describe the application of model checking to pushdown automata, in “Efficient Algorithms for Model Checking Pushdown Systems,” published in Proceedings of the Twelfth International Conference on Computer Aided Verification (CAV) (Springer Verlag, 2000), page 232, which is incorporated herein by reference. Pushdown systems are infinite transition systems having configurations of the form (control state, stack content) as their states. The authors use pushdown systems to model sequential programs with procedures by concentrating on the control flow and abstracting away information about data. The model establishes a relation between the control states of a program and the configurations of the corresponding pushdown system. Model checking is then applied to the pushdown system.