Formal verification of software source code through semi-automatic modeling

We describe the experience of modeling and formally verifying a software cache algorithm using the model checker RuleBase. Contrary to prevailing wisdom, we used a highly detailed model created directly from the C code itself, rather than a high-level abstract model.     

Memory model sensitive bytecode verification

Modern concurrent programming languages like C# and Java have a programming language level memory model, which captures the set of all allowed behaviors of programs on any implementation platform—uni- or multi-processor. Such a memory model is typically weaker than Sequential Consistency and allows reordering of operations within a program thread. Therefore, programs verified correct by assuming Sequential Consistency (that is, each thread proceeds in program order) may not behave correctly on certain platforms! One solution to this problem is to develop program checkers which are memory model sensitive. In this paper, we develop a bytecode level invariant checker for the programming language C#. Our checker identifies program states which are reached only because the C# memory model is more relaxed than Sequential Consistency. It employs partial order reduction strategies to speed up the search. These strategies are different from standard partial order reduction methods since our search also considers execution traces containing bytecode re-orderings. Furthermore, our checker identifies (a) operation re-orderings which cause undesirable states to be reached, and (b) simple program modifications—by inserting memory barrier operations—which prevent such undesirable re-orderings. A preliminary version of this paper appeared as (Huynh and Roychoudhury, in: Formal Methods Symposium, 2006). The conference paper is available from . This work was done when the first author was a Research Assistant at National University of Singapore.     

Decision-diagram-based techniques for bounded reachability checking of asynchronous systems

Bounded reachability analysis and bounded model checking are widely believed to perform poorly when using decision diagrams instead of SAT procedures. Recent research suggests this to be untrue with regards to synchronous systems and, in particular, digital circuits. This article shows that the belief is also a myth for asynchronous systems, such as models specified by Petri nets. We propose several Bounded Saturation approaches to compute bounded state spaces using decision diagrams. These approaches are based on the established Saturation algorithm, which benefits from a non-standard search strategy that is very different from breadth-first search, but employ different flavors of decision diagrams: multi-valued decision diagrams, edge-valued decision diagrams, and algebraic decision diagrams. We apply our approaches to studying deadlock as a safety property. Our extensive benchmarking shows that our algorithms often, but not always, compare favorably against two SAT-based approaches that are advocated in the literature. Research supported by the NSF under grants CNS-0501747 and CNS-0501748 and by the EPSRC under grant GR/S86211/01. An extended abstract of this article appeared in the proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS~4424, pp.~648–663, 2007, Springer.     

Embedded software verification in hardware–software codesign

Concurrent Embedded Real-Time Software (CERTS) is intrinsically different from traditional, sequential, independent, and temporally unconstrained software. The verification of software is more complex than hardware due to inherent flexibilities (dynamic behavior) that incur a multitude of possible system states. The verification of CERTS is all the more difficult due to its concurrency and embeddedness. The work presented here shows how the complexity of CERTS verification can be reduced significantly through answering common engineering questions such as when, where, and how one must verify embedded software. First, a new Schedule-Verify-Map strategy is proposed to answer the when question. Second, verification under system concurrency is proposed to answer the where question. Finally, a complete symbolic model checking procedure is proposed for CERTS verification. Several application examples illustrate the usefulness of our technique in increasing verification scalability.     

HySAT: An efficient proof engine for bounded model checking of hybrid systems

In this paper we present HySAT, a bounded model checker for linear hybrid systems, incorporating a tight integration of a DPLL–based pseudo–Boolean SAT solver and a linear programming routine as core engine. In contrast to related tools like MathSAT, ICS, or CVC, our tool exploits the various optimizations that arise naturally in the bounded model checking context, e.g.isomorphic replication of learned conflict clauses or tailored decision strategies, and extends them to the hybrid domain. We demonstrate that those optimizations are crucial to the performance of the tool.     

A classification and comparison of model checking software architecture techniques

Software architecture specifications are used for many different purposes, such as documenting architectural decisions, predicting architectural qualities before the system is implemented, and guiding the design and coding process. In these contexts, assessing the architectural model as early as possible becomes a relevant challenge. Various analysis techniques have been proposed for testing, model checking, and evaluating performance based on architectural models. Among them, model checking is an exhaustive and automatic verification technique, used to verify whether an architectural specification conforms to expected properties. While model checking is being extensively applied to software architectures, little work has been done to comprehensively enumerate and classify these different techniques.The goal of this paper is to investigate the state-of-the-art in model checking software architectures. For this purpose, we first define the main activities in a model checking software architecture process. Then, we define a classification and comparison framework and compare model checking software architecture techniques according to it.     

Efficient software product-line model checking using induction and a SAT solver

Software product line (SPL) engineering is increasingly being adopted in safety-critical systems. It is highly desirable to rigorously show that these systems are designed correctly. However, formal analysis for SPLs is more difficult than for single systems because an SPL may contain a large number of individual systems. In this paper, we propose an efficient model-checking technique for SPLs using induction and a SAT (Boolean satisfiability problem) solver. We show how an induction-based verification method can be adapted to the SPLs, with the help of a SAT solver. To combat the state space explosion problem, a novel technique that exploits the distinguishing characteristics of SPLs, called feature cube enlargement, is proposed to reduce the verification efforts. The incremental SAT mechanism is applied to further improve the efficiency. The correctness of our technique is proved. Experimental results show dramatic improvement of our technique over the existing binary decision diagram (BDD)-based techniques.     

Automatic software model checking via constraint logic

This paper proposes the use of constraint logic to perform model checking of imperative, infinite-state programs. We present a semantics-preserving translation from an imperative language with recursive procedures and heap-allocated mutable data structures into constraint logic. The constraint logic formulation provides a clean way to reason about the behavior and correctness of the original program. In addition, it enables the use of existing constraint logic implementations to perform bounded software model checking, using a combination of symbolic reasoning and explicit path exploration.     

Compositional encoding for bounded model checking

Verification techniques like SAT-based bounded model checking have been successfully applied to a variety of system models. Applying bounded model checking to compositional process algebras is, however, a highly non-trivial task. One challenge is that the number of system states for process algebra models is not statically known, whereas exploring the full state space is computationally expensive. This paper presents a compositional encoding of hierarchical processes as SAT problems and then applies state-of-the-art SAT solvers for bounded model checking. The encoding avoids exploring the full state space for complex systems so as to deal with state space explosion. We developed an automated analyzer which combines complementing model checking techniques (i.e., bounded model checking and explicit onthe-fly model checking) to validate system models against event-based temporal properties. The experiment results show the analyzer handles large systems.     

Symmetry reductions for model checking of concurrent dynamic software

Symmetry reduction techniques exploit symmetries that occur during the execution of a system in order to minimize its state space for efficient verification of temporal logic properties. This paper presents a framework for concisely defining and evaluating symmetry reductions currently used in software model checking, involving heap objects and processes. An on-the-fly state space exploration algorithm combining both techniques will also be presented. Second, the relation between symmetry and partial-order reductions is investigated, showing how ones strengths can be used to compensate for the others weaknesses. The symmetry reductions presented here were implemented in the dSPIN model-checking tool. We also performed a number of experiments that show significant progress in reducing the cost of finite-state software verification.     

Bounded model checking of infinite state systems

Bounded model checking (BMC) is an attractive alternative to symbolic model checking, since it often allows a more efficient verification. The idea of BMC is to reduce the model checking problem to a satisfiability problem of the underlying base logic, so that sophisticated decision procedures can be utilized to check the resulting formula. We present a new approach to BMC that extends current methods in three ways: First, instead of a reduction to propositional logic which restricts BMC to finite state systems, we focus on infinite state systems and therefore consider more powerful, yet decidable base logics. Second, instead of directly unwinding temporal logic formulas, we use special translations to ω-automata that take into account the temporal logic hierarchy and maintain safety and liveness properties. Third, we employ both global and local model checking procedures to take advantage of the different types of specifications that can be handled by these techniques. Based on three-valued logic, our bounded model checking procedures may either prove or disprove a specification, or they may explicitly state that no information has been obtained due to insufficient bounds.

On software verification for sensor nodes

We consider software written for networked, wireless sensor nodes, and specialize software verification techniques for standard C programs in order to locate programming errors in sensor applications before the software's deployment on motes. Ensuring the reliability of sensor applications is challenging: low-level, interrupt-driven code runs without memory protection in dynamic environments. The difficulties lie with (i) being able to automatically extract standard C models out of the particular flavours of embedded C used in sensor programming solutions, and (ii) decreasing the resulting program's state space to a degree that allows practical verification times.We contribute a platform-dependent, OS-independent software verification tool for OS-wide programs written in MSP430 embedded C with asynchronous hardware interrupts. Our tool automatically translates the program into standard C by modelling the MCU's memory map and direct memory access. To emulate the existence of hardware interrupts, calls to hardware interrupt handlers are added, and their occurrence is minimized with a double strategy: a partial-order reduction technique, and a supplementary reachability check to reduce overapproximation. This decreases the program's state space, while preserving program semantics. Safety specifications are written as C assertions embedded in the code. The resulting sequential program is then passed to CBMC, a bounded software verifier for sequential ANSI C. Besides standard errors (e.g., out-of-bounds arrays, null-pointer dereferences), this tool chain is able to verify application-specific assertions, including low-level assertions upon the state of the registers and peripherals.Verification for wireless sensor network applications is an emerging field of research; thus, as a final note, we survey current research on the topic.     

The software model checker Blast

Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast either statically proves that the program satisfies the safety property, or provides an execution path that exhibits a violation of the property (or, since the problem is undecidable, does not terminate). Blast constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. This paper gives an introduction to Blast and demonstrates, through two case studies, how it can be applied to program verification and test-case generation. In the first case study, we use Blast to statically prove memory safety for C programs. We use CCured, a type-based memory-safety analyzer, to annotate a program with run-time assertions that check for safe memory operations. Then, we use Blast to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate execution scenarios that violate the assertions for the remaining run-time checks. In our second case study, we use Blast to automatically generate test suites that guarantee full coverage with respect to a given predicate. Given a C program and a target predicate p, Blast determines the program locations q for which there exists a program execution that reaches q with p true, and automatically generates a set of test vectors that cause such executions. Our experiments show that Blast can provide automated, precise, and scalable analysis for C programs.     

Software model checking is a rich research field

This introductory paper has been written for readers who know nothing about model checking but do know about software. Its aim is to present, almost without mathematical terms, the fundamental general approaches on which the papers in this Special Section build, and give an idea of what kind of contribution each paper makes. The main issues discussed are motivation for model checking, state spaces, and bounded model checking with sat solvers. Individual papers lead to discuss the following ideas: exploiting a distributed computing environment for model checking, constructing those states first that look most promising for eventually finding errors, only constructing a representative subset of states, the representation of contents of variables in an abstract way with approximation from below, and the use of more general solvers than sat solvers in bounded model checking.     

Verifying the summit bus converter protocols with symbolic model checking

We report on our investigation of a new verification tool, the Symbolic Model Verifier (SMV), created at Carnegie Mellon University. We have successfully, employed this tool to detect deadlock in an industrial design, namely, Hewlett-Packard's Summit bus converter chips. In addition to locating a known deadlock in the original chip design and checking its solution, we successfully detected other previously unknown defects in the design. In our experiments, we were able to verify properties on finite-state models of the circuit with 150 to 200 state variables in a matter of minutes.     

The formal-CAFE methodology and model checking patterns in the specification of e-commerce systems

Electronic commerce is an important application that has evolved significantly recently. However, electronic commerce systems are complex and difficult to be correctly designed. Guaranteeing the correctness of an e-commerce system is not an easy task due to the great amount of scenarios where errors occur, many of them very subtle. In this work we presents a methodology that uses formal-method techniques, specifically symbolic model checking, to design electronic commerce applications and to automatically verify them. Also, a model checking pattern hierarchy has been developed—it specifies patterns to construct and verify the formal model of e-commerce systems. We consider this research the first step to the development of a framework, which will integrate the methodology, an e-commerce specification language based on business rules, and a model checker. Adriano Pereira received the B.S. and M.S. degrees in computer science in 2000 and 2002, respectively, and he is currently pursuing the Ph.D. degree in computer science from the Federal University of Minas Gerais, Belo Horizonte, Brazil. His current interests are on performance analysis and modeling of e-business and distributed systems, and formal methods. Mark Song received the B.S., M.S. and Ph.D. degrees in computer science from the Federal University of Minas Gerais, Belo Horizonte, Brazil. His current interests are on distributed systems and formal methods – especially BMC (Bounded Model Checking). Gustavo Franco received the B.S. and M.S. degrees in computer science in 2001 and 2004, respectively, from the Federal University of Minas Gerais, Belo Horizonte, Brazil. His research was on modeling the user behavior of e-business and distributed systems, and formal methods. Actually his current interests are on software engeneering and project management of IT projects.     

Automated formal verification of visual modeling languages by model checking

Graph transformation has recently become more and more popular as a general, rule-based visual specification paradigm to formally capture (a) requirements or behavior of user models (on the model-level), and (b) the operational semantics of modeling languages (on the meta-level) as demonstrated by benchmark applications around the Unified Modeling Language (UML). The current paper focuses on the model checking-based automated formal verification of graph transformation systems used either on the model-level or meta-level. We present a general translation that inputs (i) a metamodel of an arbitrary visual modeling language, (ii) a set of graph transformation rules that defines a formal operational semantics for the language, and (iii) an arbitrary well-formed model instance of the language and generates a transitions system (TS) that serve as the underlying mathematical specification formalism of various model checker tools. The main theoretical benefit of our approach is an optimization technique that projects only the dynamic parts of the graph transformation system into the target transition system, which results in a drastical reduction in the state space. The main practical benefit is the use of existing back-end model checker tools, which directly provides formal verification facilities (without additional efforts required to implement an analysis tool) for many practical applications captured in a very high-level visual notation. The practical feasibility of the approach is demonstrated by modeling and analyzing the well-known verification benchmark of dining philosophers both on the model and meta-level.