Model Checking Software

As time goes by, it becomes more and more apparent that the puzzles of life involve more and more molecular pieces that fit together in increasingly complex ways. Biology is not an exact science. It is messy and noisy, and most often vague and ambiguous. We cannot assign clear rules to the way cells behave and interact with one another, and we often cannot quantify the exact amounts of molecules, such as genes and proteins, in the resolution of a single cell. To make matters worse (so to speak), the combinatorial complexity observed in biological networks is staggering, which renders the comprehension and analysis of such systems a major challenge. Recent efforts to create executable models of complex biological phenomena - an approach called Executable Biology - entail great promise for new scientific discoveries, shading new light on the puzzle of life. At the same time, this ’new wave of the future’ forces Computer Science to stretch far and beyond, and in ways never considered before, in order to deal with the enormous complexity observed in biology. In this talk, I will summarize some of the success stories in using formal verification to reason about mechanistic models in biology. In particular, I will focus on models of cell fate decisions during normal development, organogenesis, and cancer, and their analysis using model checking. If time permits, I will also mention some of the major milestones on the way to conquer biological complexity.

When analyzing the behavior of finite-state concurrent systems by model checking, one way of fighting state explosion is to reduce the model as much as possible whilst preserving the properties under verification. We consider the framework of action-based systems, whose behaviors can be represented by labeled transition systems (Ltss), and whose temporal properties of interest can be formulated in modal μ-calculus (L _μ ). First, we determine, for any L _μ formula, the maximal set of actions that can be hidden in the Lts without changing the interpretation of the formula. Then, we define \(L_\mu^{\it dsbr}\), a fragment of L _μ which is compatible with divergence-sensitive branching bisimulation. This enables us to apply the maximal hiding and to reduce the Lts on-the-fly using divergence-sensitive τ-confluence during the verification of any \(L_\mu^{\it dsbr}\) formula. The experiments that we performed on various examples of communication protocols and distributed systems show that this reduction approach can significantly improve the performance of on-the-fly verification.

Verifying string manipulating programs is a crucial problem in computer security. String operations are used extensively within web applications to manipulate user input, and their erroneous use is the most common cause of security vulnerabilities in web applications. Unfortunately, verifying string manipulating programs is an undecidable problem in general and any approximate string analysis technique has an inherent tension between efficiency and precision. In this paper we present a set of sound abstractions for strings and string operations that allow for both efficient and precise verification of string manipulating programs. Particularly, we are able to verify properties that involve implicit relations among string variables. We first describe an abstraction called regular abstraction which enables us to perform string analysis using multi-track automata as a symbolic representation. We then introduce two other abstractions—alphabet abstraction and relation abstraction—that can be used in combination to tune the analysis precision and efficiency. We show that these abstractions form an abstraction lattice that generalizes the string analysis techniques studied previously in isolation, such as size analysis or non-relational string analysis. Finally, we empirically evaluate the effectiveness of these abstraction techniques with respect to several benchmarks and an open source application, demonstrating that our techniques can improve the performance without loss of accuracy of the analysis when a suitable abstraction class is selected.

This paper focuses on reducing memory usage in enumerative model checking, while maintaining the multi-core scalability obtained in earlier work. We present a multi-core tree-based compression method, which works by leveraging sharing among sub-vectors of state vectors.

An algorithmic analysis of both worst-case and optimal compression ratios shows the potential to compress even large states to a small constant on average (8 bytes). Our experiments demonstrate that this holds up in practice: the median compression ratio of 279 measured experiments is within 17% of the optimum for tree compression, and five times better than the median compression ratio of Spin’s Collapse compression.

Our algorithms are implemented in the LTSmin tool, and our experiments show that for model checking, multi-core tree compression pays its own way: it comes virtually without overhead compared to the fastest hash table-based methods.

We present algorithms to efficiently bound the depth of the state spaces explored by explicit-state model checkers. Given a parameter k, our algorithms guarantee finding any violation of an invariant that is witnessed using a counterexample of length k or less from the initial state. Though depth bounding is natural with breadth-first search, explicit-state model checkers are unable to use breadth first search due to prohibitive space requirements, and use depth-first search to explore large state spaces. Thus, we explore efficient ways to perform depth bounding with depth-first search. We prove our algorithms sound (in the sense that they explore exactly all the states reachable within a depth bound), and show their effectiveness on large real-life models from Microsoft’s product groups.

While exhaustive state space traversal is not feasible in reasonable time for complex concurrent programs, many techniques for efficient detection of concurrency errors and testing of concurrent programs have been introduced in recent years, such as directed search and context-bounded model checking.

We propose to use depth-first traversal with randomized backtracking, where it is possible to backtrack from a state before all outgoing transitions have been explored, and the whole process is driven by random number choices. Experiments with a prototype implementation in JPF on several Java programs show that, in most cases, fewer states must be explored to find an error with our approach than using the existing techniques.

This paper describes how new language features can be seamlessly added to an extensible specification of Promela to provide new (domain-specific) notations and analyses to the engineer. This is accomplished using ableP, an extensible specification and implementation of Promela, the modeling language used by the spin model checker. Language extensions described here include an enhanced select-statement, a convenient tabular notation for boolean expressions, a notion of discrete time, and extended type checking. ableP and the extensions are developed using the Silver attribute grammar system and the Copper parser and scanner generator. These tools support the modular development and composition of language extensions so that independently developed extensions can be imported into ableP by an engineer with little knowledge of language design and implementation issues.

Sketching is an approach to automated software synthesis where the programmer develops a partial implementation called a sketch and a separate specification of the desired functionality. A synthesizer tool then automatically completes the sketch to a complete program that satisfies the specification. Previously, sketching has been applied to finite programs with a desired functional input/output behavior and given invariants. In this paper, we consider (non-terminating) reactive programs and use the full branching time logic CTL* to formalize specifications. We show that the sketching problem can be reduced to a CTL* model checking problem provided there is a translation of the program to labeled transition systems.

This paper addresses the problem of verifying and correcting programs when they are moved from a sequential consistency execution environment to a relaxed memory context. Specifically, it considers the TSO (Total Store Order) relaxation, which corresponds to the use of store buffers, and its extension x86-TSO, which in addition allows synchronization and lock operations.

The proposed approach uses a previously developed verification tool that uses finite automata to symbolically represent the possible contents of the store buffers. Its starting point is a program that is correct for the usual sequential consistency memory model, but that might be incorrect under x86-TSO. This program is then analyzed for this relaxed memory model and when errors are found (with respect to safety properties), memory fences are inserted in order to avoid these errors. The approach proceeds iteratively and heuristically, inserting memory fences until correctness is obtained, which is guaranteed to happen.

An advantage of our technique is that the underlying symbolic verification tool makes a full exploration possible even for cyclic programs, which makes our approach broadly applicable. The method has been tested with an experimental implementation and can effectively handle a series of classical examples.

Modern production plants are highly automated complex systems consisting of several robots and other working machines. Errors leading to damage and stop of production are extremely expensive and must be avoided by all means. Hence, the state of practice is to test control programs in advance which implies high effort and comes with high costs. To increase the confidence into the control systems and to reduce the necessary effort, this paper proposes to use model checking to verify certain properties. It presents a compiler that can transform industrial robot programs into PROMELA models. Since the statements of the robot programming language can not be mapped directly into PROMELA statements, we apply compiler optimization techniques to close the semantic gap. In case of a specification violation the trace is mapped to the original context so that the robot programmer can reconstruct the problem. As a case study we applied the tool to verify the absence of collisions and deadlocks. We were able to detect one deadlock in a car-body welding station with 9 robots, correct the program and verify the correctness of the resulting system.

This paper presents EpiSpin: an Eclipse plug-in for editing Promela models. It provides error markers as you type, various editor services and an interface to perform verification and simulation runs using Spin. An additional tool shows the static relations between channels, processes and global variables. These tools have been built using the Spoofax language workbench.

The computation of counterexamples for probabilistic model checking has been an area of active research over the past years. In spite of the achieved theoretical results in this field, there is no freely available tool that allows for the computation and representation of probabilistic counterexamples. We present an open source tool called DiPro that can be used with the PRISM and MRMC probabilistic model checkers. It allows for the computation of probabilistic counterexamples for discrete time Markov chains (DTMCs), continuous time Markov chains (CTMCs) and Markov decision processes (MDPs). The computed counterexamples can be rendered graphically.

In order to improve quality of an implementation of a distributed and multithreaded system, software engineers inspect code and run tests. However, the concurrent nature of such systems makes these tasks challenging. For testing, this problem is addressed by stress testing, which repeatedly executes a test hoping that eventually all possible outcomes of the test will be encountered.