The development of modern software systems involves a rich collection of software artifacts. Artifacts may represent aspects of the process by which software is developed or the various products that are outcomes of stages of process phases. Disciplined approaches to software development will apply criteria to determine essential properties of such artifacts, for example, a requirements model should be checked for completeness and consistency prior to commencement of system design. For large complex software systems, such criteria should be formalized and their checks automated. While reasoning about structural properties of artifacts is efficient and can be useful (e.g., checking interface signatures), behavioral reasoning is the ultimate goal.
The potential of model checking technology for: (a) detecting coding flaws that are hard to detect using existing quality assurance methods (e.g., such as bugs that arise from unanticipated interleavings in concurrent programs), and (b) verifying that system models and implementations satisfy crucial temporal properties and other light-weight specifications has led a number of international corporations and government research labs such as Microsoft,IBM, Lucent, NEC, NASA, and Jet Propulsion Laboratories (JPL) to fund their own software model checking projects.
The effectiveness of the software model checking applications cited above has in most cases relied on the fact that the researchers carrying out the studies had a detailed knowledge of the model checking tool being applied and understood very clearly (perhaps as the result of extensive experimentation) how to (a) map the problem being modeled to the tool in a manner that would draw on the strengths of the tool, and (b) how to configure the tool for optimal performance. In some cases, researchers were not satisfied with the results of mapping their problem to an available configuration of an existing tool, and they found it necessary to study an existing model checking framework in detail in order to customize it. In other cases, researchers had the insight that they needed to develop a new framework targeted to the semantics of a family of artifacts (e.g., JPF for Java programs) or a specific domain (e.g., SLAM for device drivers).
We believe that a number of trends both in the requirements of computing systems and in the processes by which they are developed that will drive persons and organizations interested in applying model checking technology to rely increasingly on customization/adaptation of existing tool frameworks or construction of new model checking tools.
Model-driven development: Increasing emphasis on using a rich collection of interlinked models at a variety of levels of abstraction for not only software design but also software implementation will drive researchers to look beyond model checkers with fixed input languages that target a single level of abstraction. Current technology allows model checking to be applied at the source code and byte code (or machine code level) as well as higher level models -- but for the most part, different tools with different characteristics are used for these different levels of abstraction. We envision a single integrated framework in which artifacts at all levels of abstraction are checkable, in which relationships such as refinement/conformance are established by model checking collections of artifacts at different levels of abstraction, and in which verification models are formed by composing: (a) analyzable models from which code is automatically generated, (b) manually written source that was not amenable to auto-generation, and (c) high-level specifications of cross-cutting aspects such as synchronization or event delivery policies.
Product-line architectures and reusable middleware infrastructure: Large-scale distributed systems are increasingly built on top of middleware frameworks such as CORBA and .NET and use software product-line architectures that encourage the reuse of software components and infrastructure across applications. The size (often 100's of thousands of lines of code) and the complexity of this infrastructure (which often contains extensive use of object-oriented design patterns and complex heap structures) will make it difficult to apply existing techniques for model-extraction from source code, but the high degree of reuse of this infrastructure will make it feasible to construct custom-built verification model components and checking engines that are tailored to those frameworks. Moreover, as greater automation is sought in development and validation processes, developers will have a greater difficulty applying general purpose model checking tools which require a higher degree of configuration and interaction, and product-line architects will increasingly seek to reduce developer involvement by building model checking infrastructure that is dedicated to a particular software architecture, domain, and development process.
Sheer variety of application domains and computation models: As software is embedded in an ever broadening range of devices and as software increases in scale, verification experts will increasingly move away from general purpose solutions as they seek to achieve scalability by developing search algorithms, state-storage approaches, and model reduction strategies that leverage properties of a particular domain. For example, we have observed that reduction methods designed for a particular application domain (e.g., for example, Java programs) may be ineffective for a different application domain such as avionics systems where timing issues play a greater role. Conversely, we have found that the specialized quasi-cyclic structure of computation in a certain class of avionics systems enables dramatic optimizations in state space search and state storage strategies that are customized for this particular domain.
Thus, there is a need for model checking tools that support customization, extensibility, and that are easily embedded or encapsulated in larger development tools. Existing model checkers, however, including widely used tools such as SPIN , FDR2 , and NuSMV , are designed to support a fixed input language using a fixed collection of state-space representations, reduction and exploration algorithms. The capabilities of these tools have evolved over time, but that evolution has been limited to the capabilities that the tool developer themselves found useful or desirable. Moreover, most existing tools do not provide direct support for features found in object-oriented software systems. Recent versions of the SPIN model checker allow one to include C source directly in the Promela modeling language. While this does allow for a degree of extensibility, one might benefit more from comprehensive mechanisms for extensibility that are part of the overall design of the model checking framework.
While it is possible to continue the practice of cannibalizing and modifying existing model checkers, or building new model checkers from scratch, the level of knowledge and effort required for such activitivies currently prevents many domain experts who are not necessarily experts in model checking from successfully applying model checking to software analysis. Even though experts in different areas of software engineering have significant domain knowledge about the semantic primitives and properties of families of artifacts that could be brought to bear to produce cost-effective semantic reasoning via model checking, in order to make effective use of model checking technology these experts should not be required to build their own model checker or to pour over the details of an existing model checker implementation while carrying out substantial modifications.