Search

The Specification Pattern System (SPS) and the Property Specification (Prospec) tool assist a user in generating formal specifications in Linear Temporal Logic (LTL), as well as other languages, from property patterns and scopes. Patterns are high-level abstractions that provide descriptions of common properties, and scopes describe the extent of program execution over which the property holds. The purpose of the work presented in this paper is to verify that the generated LTL formulas match the natural language descriptions, timelines, and traces of computation that describe the pattern and scope. The LTL formulas were verified using the Spin model checker on test cases developed using boundary value analysis and equivalence class testing strategies. A test case is an LTL formula and a sequence of Boolean valuations. The LTL formulas were those generated from SPS and Prospec. The Boolean valuations of propositions in the LTL formula are generated by a deterministic, single-threaded Promela program that was run using the software model-checker Spin. For each pattern, a suite of test cases was. The experiments uncovered several errors in both the SPS-generated and the Prospec-generated formulas. [ABSTRACT FROM AUTHOR]

The language χ is a modeling and simulation language which is currently mainly used to analyse and optimize the performance of industrial systems. To be able to also verify functional properties of a system using a χ model, part of the language has been given a formal semantics. Rather than implementing a new model checker for χ, the philosophy is to provide automatic translations from χ into the specification languages of existing state-of-the-art model checkers such as, e.g., spin and uppaal. In this paper, we propose for χ a notion of stuttering congruence, which is an adaptation of the notion of stuttering equivalence. We prove that our notion preserves the validity of ctl∗-× formulas, that it preserves deadlock, and that it is indeed a congruence with respect to the constructs of χ. We also indicate how our notion is to be used to establish confidence in the correctness of a translation from χ into promela. [ABSTRACT FROM AUTHOR]

Despite significant advances in the development of model checking, it remains a difficult task in the hands of experts to make it scale to the size of industrial systems. A key step in achieving scalability is to "divide-and-conquer", that is, to break up the veri.cation of a system into smaller tasks that involve the verification of its components. Assume-guarantee reasoning [9, 11] is a widespread "divide-and-conquer" approach that uses assumptions when checking individual components of a system. Assumptions essentially encode expectations that each component has from the rest the system in order to operate correctly. Coming up with the right assumptions is typically a non-trivial manual process, which limits the applicability of this type of reasoning in practice. [ABSTRACT FROM AUTHOR]

Conventional software model-checking involves (i) creating an abstract model of a complex application; (ii) validating this model against the application; and (iii) checking safety properties against the abstract model. To non-experts, steps (i) and (ii) are often the most daunting. Firstly how does one decide which aspects of the application to include in the abstract model? Secondly, how does one determine whether the abstraction inadvertently "hides" critical bugs? Similarly, if a counter-example is found, how does one determine whether this is a genuine bug or just a modelling artifact? [ABSTRACT FROM AUTHOR]

3Spin and 3Murphi are modified versions of the Spin model checker and the Murϕ verifier. Our modifications enhance the probabilistic algorithms and data structures for storing visited states, making them more effective and more usable for verifying huge transition systems. The tools also support a verification methodology designed to minimize time to finding errors, or to reaching desired certainty of error-freedom. This methodology calls for bitstate hashing, hash compaction, and integrated analyses of both to provide feedback and advice to the user. 3Spin and 3Murphi are the only tools to offer this support, and do so with the most powerful and flexible currently-available implementations of the underlying algorithms and data structures. [ABSTRACT FROM AUTHOR]

We present Etch, an enhanced type checking tool for the Promela language. This tool uses standard type checking in conjunction with constraint-based type inference to detect type errors in Promela models which cannot currently be detected by Spin before verification or simulation. Etch allows for more rapid development of Promela code, and increased confidence in verification models used with Spin. Since the utility of model checking depends heavily on the correctness of the model being verified, our tool is a significant contribution. [ABSTRACT FROM AUTHOR]

Embedded software verification is an important verification problem that requires the ability to reason about the timed semantics of concurrent behaviors at a low level of atomicity. Combining a cycle-accurate debugger with model checking algorithms provides an accurate model of software execution at the machine-code level while supporting concurrency and allowing abstractions to manage state explosion. We report on the design and implementation of such a model checker using the GNU debugger (gdb) with different processor backends. A significant feature of the resulting tool is that we can adjust the level of atomicity during the model checking run to reduce state explosion while focusing on behaviors that are likely to generate an error. [ABSTRACT FROM AUTHOR]

Advanced attack sequences combine different kinds of steps (e.g. attacker, protocol, and administration steps) on multiple networked systems. We propose a SPIN based approach for formal modeling and analysis of such scenarios. Our approach is especially suited for scenarios were protocol and network level aspects matter simultaneously. Typical attack sequences and not yet considered variants can be automatically found. The development of scenario models is supported by a modeling framework and the use of the high-level process specification language cTLA. A compiler translates the high-level cTLA models to Promela. This allows the powerful model-checking tool SPIN to be employed for analysis. Through integration of the compiler and SPIN into the Eclipse platform both model development and analysis are facilitated. [ABSTRACT FROM AUTHOR]

Security protocols are notoriously difficult to debug. One approach to the automatic verification of security protocols with a bounded set of agents uses logic programming with analysis and synthesis rules to describe how the attacker gains information and constructs new messages. We propose a generic approach to verifying security protocols in Spin. The dynamic process creation mechanism of Spin is used to nondeterministically create different combinations of role instantiations. We incorporate the synthesis and analysis features of the logic programming approach to describe how the intruder learns information and replays it back into the system. We formulate a generic "loss of secrecy" property that is flagged whenever the intruder learns private information from an intercepted message. We also describe a simplification of the Dolev-Yao attacker model that suffices to analyze secrecy properties. [ABSTRACT FROM AUTHOR]

Emptiness check is a key operation in the automata-theoretic approach to LTL verification. However, it is usually done on Büchi automata with a single acceptance condition. We review existing on-the-fly emptiness-check algorithms for generalized Büchi automata (i.e., with multiple acceptance conditions) and show how they compete favorably with emptiness-checks for degeneralized automata, especially in presence of weak fairness assumptions. We also introduce a new emptiness-check algorithm, some heuristics to improve existing checks, and propose algorithms to compute accepting runs in the case of multiple acceptance conditions. [ABSTRACT FROM AUTHOR]

In this work, we focus on hierarchical component systems. We describe both the functional behaviour and the non-functional features (life-cycle management) of components in terms of synchronised transition systems; functional behaviours are supposed to be specified by the component developer, while management features can be built automatically for the architecture definition of a given component system. We define a notion of correct component composition; then we show how we can prove, using (compositional) model-checking techniques, temporal properties of a component system. Transformations of a system, for example replacement of a sub-component, are expressed as transformations of its behavioural semantics, allowing to prove preservation of some properties, or the validity of new properties after transformation. [ABSTRACT FROM AUTHOR]

Recently, an active research topic in software verification is applying model checkers to programs, such as multi-threaded Java code. However, a program typically consists of more behaviors, such as operations on complicated data structures or implementation details which are typically made for some criteria like performance. A brute-force model extraction may produce a poor model for analysis engine. In this paper, we give examples to show how subtle changes in implementation may result in considerable differences in analysis, particularly to compositional analysis. Unfortunately, these implementation choices are made by programmers - people who typically do not possess the knowledge of verification. To mitigate such sensitivity, we advocate that verification tools should recognize and support abstract data types and, in the meantime, prohibit or suppress the use of array. Programming process behaviors with abstract data types can hide and converge the implementation choices. More importantly, abstract data types are informative. They provide essential information for tool automation to select a best implementation for analysis. In this paper, we describe the design and implementation of such a prototype tool which can parse systems written in Promela syntax. [ABSTRACT FROM AUTHOR]

We present a novel algorithm for repairing structurally complex data. Given an assertion that represents desired structural integrity constraints and a structure that violates them, the algorithm performs repair actions that mutate the given structure to generate a new structure that satisfies the constraints. Assertions are written as imperative predicates, which can express rich structural properties. Since these properties can be arbitrarily complex, our algorithm is sound but not complete, and it may not terminate in certain cases. Experimental results with our prototype implementation, Juzi, show that it is feasible to efficiently repair a variety of complex data structures that are routinely used in library code. Juzi can often repair structures comprising of over a hundred objects (even when majority of the objects have some corrupted field) in less than one second. Our algorithm is based on systematic backtracking but does not require storing states and can easily be implemented in a variety of software model checkers, such as the Java PathFinder, SPIN, and VeriSoft. [ABSTRACT FROM AUTHOR]

Partial-order reduction is widely used to alleviate state-space explosion in model checkers for concurrent programs. Traditional approaches to partial-order reduction are based on ample sets. Natural ample sets can be computed for threads that communicate with each other predominantly through message queues. For threads that communicate with shared memory using locks for synchronization, Lipton's theory of reduction provides a promising way to aggregate several fine-grained transitions into larger transactions. In traditional partial-order reduction, actions that are not in the ample set are delayed, thus avoiding the redundant exploration of equivalent interleaving orders. Delaying the execution of actions indefinitely can lead to loss of soundness. This is called the ignoring problem. The usual solution to the ignoring problem is by Cycle Detection. Explicit state model checkers usually use Depth First Search, and when a cycle is detected, disallow using a reduced ample set that closes the cycle. The ignoring problem exists in transaction-based reduction as well. We present a novel solution to the ignoring problem in the context of transaction-based reduction. We designate certain states as commit points and track the exploration to discover whether the reduced exploration guarantees a path from each commit point to a state where the transaction is completed. If such a path does not exist, we detect this at the time a commit point is popped from the stack, and schedule all threads at the commit point. This paper presents our algorithm, called Commit Point Completion (CPC). We have implemented both CPC and Cycle Detection in the Zing model checker, and find that the CPC algorithm performs better. [ABSTRACT FROM AUTHOR]

We describe an improvement of the partial-order reduction algorithm for breadth-first search which was introduced in Spin version 4.0. Our improvement is based on the algorithm by Alur et al. for symbolic state model checking for local safety properties [1]. The crux of the improvement is an optimization in the context of explicit state model checking of the condition that prevents action ignoring, also known as the cycle proviso. There is an interesting duality between the cycle provisos for the breadth-first search (BFS) and depth first search (DFS) exploration of the state space, which is reflected in the role of the BFS queue and the DFS stack, respectively. The improved version of the algorithm is supported in the current version of Spin and can be shown to perform significantly better than the initial version. [ABSTRACT FROM AUTHOR]

Software model checking problems generally contain two different types of non-determinism: 1) non-deterministically chosen values; 2) the choice of interleaving among threads. Most modern software model checkers can handle only one source of non-determinism efficiently, but not both. This paper describes a SAT-based model checker for asynchronous Boolean programs that handles both sources effiectively. We address the first type of non-determinism with a form of symbolic execution and fix-point detection. We address the second source of non-determinism using a symbolic and dynamic partial-order reduction, which is implemented inside the SAT-solver's case-splitting algorithm. The preliminary experimental results show that the new algorithm outperforms the existing software model checkers on large benchmarks. [ABSTRACT FROM AUTHOR]

In precursory work we suggested an abstraction-based highly scalable semi-test for the boundedness of Communicating Finite State Machine (CFSM) based modelling and programming languages. We illustrated its application to Promela and UML-RT models. The test is sound with respect to determining boundedness, but may return inconclusive "counterexamples" when boundedness cannot be established. In this paper we turn to the question how to effectively determine the spuriousness of these counterexamples, and how to refine the abstraction based on the analysis. We employ methods from program analysis and illustrate the application of our refinement method to a number of Promela examples. [ABSTRACT FROM AUTHOR]

The limited amount of memory is the major bottleneck in model checking tools based on an explicit states enumeration. In this context, techniques allowing an efficient representation of the states are precious. We present in this paper a novel approach which enables to store the state space in a compact way. Though it belongs to the family of explicit storage methods, we qualify it as semi-explicit since all states are not explicitly represented in the state space. Our experiments report a memory reduction ratio up to 95% with only a tripling of the computing time in the worst case. [ABSTRACT FROM AUTHOR]

The most expensive operation in explicit state model checking is the hash computation required to store the explored states in a hash table. One way to reduce this computation is to compute the hash incrementally by only processing those portions of the state that are modified in a transition. This paper presents an incremental heap canonicalization algorithm that aids in such an incremental hash computation. Like existing heap canonicalization algorithms, the incremental algorithm reduces the state space explored by detecting heap symmetries. On the other hand, the algorithm ensures that for small changes in the heap the resulting canonical representations differ only by relatively small amounts. This reduces the amount of hash computation a model checker has to perform after every transition, resulting in significant speedup of state space exploration. This paper describes the algorithm and its implementation in two explicit state model checkers, CMC and Zing. [ABSTRACT FROM AUTHOR]

This paper presents a technique that uses code to automatically generate its own test cases at run time by using a combination of symbolic and concrete (i.e regular) execution The input values to a program (or software component) provide the standard interface of any testing framework with the program it is testing and generating input values that will explore all the "interesting" behavior in the tested program remains an important open problem in software testing research. Our approach works by turning the problem on its head: we lazily generate from within the program itself the input values to the program (and values derived from input values) as needed. We applied the technique to real code and found numerous corner case errors ranging from simple memory overflows and infinite loops to subtle issues in the interpretation of language standards. [ABSTRACT FROM AUTHOR]

We review and discuss the current approaches to software model checking, including the complementary views of validation versus falsification and those of static versus dynamic analysis. For falsification, also known as bug finding, we advocate the need for blended approaches that combine the strengths of both static and dynamic analysis. We outline possible directions of research in this area. [ABSTRACT FROM AUTHOR]

Blast is a verification system for checking safety properties of C programs. Blast implements a lazy-abstraction algorithm, which integrates automatic abstraction refinement and model checking [8]. The input to Blast is a C program and a safety monitor written in a specification language with C like syntax [1]. The lazy-abstraction algorithm returns either an error trace of the program together with a corresponding test case [2], or a proof that the program satisfies the safety property [6] (or, since the problem is undecidable, the algorithm may fail to terminate). Blast automatically constructs and refines a parsimonious predicate abstraction of the input program, using an interpolation-based decision procedure to find, based on counterexample analysis, the relevant predicates for each individual control location [5]. Blast has successfully verified and found violations of interface safety properties of large device driver programs [6,5], memory safety properties [3], race conditions in nesC programs (using an extension for concurrent programs) [4], and file handling properties of large open-source programs [9]. Extensions to Blast support program testing [2] and incremental programming [7]. Blast is available from http://www.eecs.berkeley.edu/ blast. [ABSTRACT FROM AUTHOR]

In recent years there has been an increasing move towards analyzing software programs with the aid of model checking. In this tutorial we will focus on one of the first model checkers developed specifically for analyzing programs - Java PathFinder (JPF). JPF was awarded the 2003 Engineering Innovation award from NASA's Office of Aerospace Technology. JPF is freely available and the development became an open-source project in April 2005http://javapathfinder.sourceforge.net. JPF has been used on numerous NASA applications, including, Mars Rover control, Deep-Space 1 fault protection, and Shuttle ground control software as well as on software from companies such as Fujitsu. [ABSTRACT FROM AUTHOR]

This tutorial consists of two parts. In the first part we present an advanced overview of Spin [1][4], and illustrate its practical application to logic model checking problems. In the second part of the tutorial we present an overview of a related tool called Modex [2,3]. Modex can be used to extract Spin verification models directly from C source code. It supports the definition of user-defined abstractions, and cleverly exploits the capability in Spin version 4 to include embedded C code inside abstract verification models. We will show how to use Spin and Modex, separately and combined, in an effective way when searching for design errors in distributed software applications. Both Spin and Modex are written in ANSI-C and can freely be used on research projects. [ABSTRACT FROM AUTHOR]

One of the key challenges for computer security is the problem of software security: how to build software that is free of implementation vulnerabilities. In this talk, I will present experience with pushdown model checking for software security. First, I will survey simple methods for pushdown model checking, and I will introduce MOPS, a tool for pushdown model checking of C programs. Then, I will show many security properties of interest may be encoded as temporal safety properties that are well-suited to analysis with model checking. I will report on our experience applying MOPS to tens of millions of lines of C code. Finally, I will discuss some possible directions for future research. [ABSTRACT FROM AUTHOR]