Concurrency errors are notoriously difficult to debug because they may occur only under unexpected thread interleavings that are difficult to identify and reproduce. These errors are increasingly important as recent hardware trends compel developers to write more concurrent software and to provide more concurrent abstractions. This thesis presents algorithms that dynamically and systematically explore a program's thread interleavings to manifest concurrency bugs quickly and reproducibly, and to provide precise incremental coverage guarantees. Dynamic concurrency testing tools should provide (1) fast response -- bugs should manifest quickly if they exist, (2) reproducibility -- bugs should be easy to reproduce and (3) coverage -- precise correctness guarantees when no bugs manifest. In practice, most tools provide either fast response or coverage, but not both. These goals conflict because a program's thread interleavings exhibit exponential state- space explosion, which inhibits fast response. Two approaches from prior work alleviate state-space explosion. (1) Partial-order reduction provides full coverage by exploring only one interleaving of independent transitions. (2) Bounded search provides bounded coverage by enumerating only interleavings that do not exceed a bound. Bounded search can additionally provide guarantees for cyclic state spaces for which dynamic partial-order reduction provides no guarantees. Without partial-order reduction, however, bounded search wastes most of its time exploring executions that reorder only independent transitions. Fast response with coverage guarantees requires both approaches, but prior work failed to combine them soundly. We combine bounded search with partial-order reduction and extensively analyze the space of dynamic, bounded partial-order reduction strategies. First, we prioritize with a best-first search and show that heuristics that combine these approaches find bugs quickly. Second, we restrict partial-order reduction to combine approaches while maintaining bounded coverage. We specialize this approach for several bound functions, prove that these algorithms guarantee bounded coverage, and leverage dynamic information to further reduce the state space. Finally, we bound the partial order on a program's transitions, rather than the total order on those transitions, to combine these approaches without sacrificing partial-order reduction. This algorithm provides fast response, incremental coverage guarantees, and reproducibility. We manifest bugs an order of magnitude more quickly than previous approaches and guarantee incremental coverage in minutes or hours rather than weeks, helping developers find and reproduce concurrency errors. This thesis makes bounded stateless model checking for concurrent programs substantially more efficient and practical. / text

University, Diss., 2002--Kiel.

Concurrent data structures have found increasingly widespread use in both multicore and distributed computing environments, thereby escalating the priority for verifying their correctness. The thread safe behavior of these concurrent objects is often described using formal semantics known as linearizability, which requires that  every operation in a concurrent object appears to take effect between its invocation and response. Quasi linearizability is a quantitative relaxation of linearizability to allow more implementation freedom for performance optimization.  However, ensuring the quantitative aspects of this new correctness condition is an arduous task. We propose the first method for formally verifying quasi linearizability of the implementation model of a concurrent data structure. The method is based on checking the refinement relation between the implementation model and a specification model via explicit state model checking. It can directly handle multi-threaded programs where each thread can make infinitely many method calls, without requiring the user to manually annotate for the linearization points. We have implemented and evaluated our method in the PAT model checking toolkit.  Our experiments show that the method is effective in verifying quasi linearizability and in detecting its violations. / Master of Science

Disk based model checking does not receive much attention in the model checking field becasue of its costly time overhead. In this thesis, we present a new disk based algorithm that can get close to or faster verification speed than a RAM based algorithm that has enough memory to complete its verification. This algorithm also outperforms Stern and Dill's original disk based algorithm. The algorithm partitions the state space to several files, and swaps files into and out of memory during verification. Compared with the RAM only algorithm, the new algoritm reduces hash table insertion time by reducing the cost and growth of the hash load. Compared with Stern's disk based algorithm, the new disk based algorithm significantly reduces disk vs memory comparsion but increases disk read/write time. The size of the model the new algorithm can verify is bound to the available disk size instead of the available RAM size.

Formal verification methods offer a large potential to provide automated software correctness checking (based on sound mathematical roots), which is of vital importance. One such technique is abstract regular model checking, which encodes sets of reachable configurations and one-step transitions between them using finite automata and transducers, respectively. Though this method addresses problems that are undecidable in general, it facilitates termination in many practical cases, while also significantly reducing the state space explosion problem. This is achieved by accelerating the computation of reachability sets using incrementally refinable abstractions, while eliminating spurious counterexamples caused by overapproximation using a counterexample-guided abstraction refinement technique. The aim of this thesis is to create a well designed tool for abstract regular model checking, which has so far only been implemented in prototypes. The new tool will model systems using symbolic automata and transducers instead of their (less concise) classic alternatives.

Template semantics is a template-based approach to describing the semantics of model-based notations, where a pre-defined template captures the notations' common semantics, and parameters specify the notations' distinct semantics. In this thesis, we investigate using template semantics to parameterize the translation from a model-based notation to the input language of the SMV family of model checkers. We describe a fully automated translator that takes as input a specification written in template semantics syntax, and a set of template parameters, encoding the specification's semantics, and generates an SMV model of the specification. The result is a parameterized technique for model checking specifications written in a variety of notations. Our work also shows how to represent complex composition operators, such as rendezvous synchronization, in the SMV language, in which there is no matching language construct.

Cette thèse a eu pour but l'étude et la mise en oeuvre des méthodes de vérification par abstraction pour les modèles AltaRica. A cette effet, une méthode d'abstraction permettant l'utilisation d'une sous approximation de l'espace des états d'un système dans un algorithme CEGAR est présentée. Son utilisation permet d'accélérer l'algorithme CEGAR, ainsi que de réduire les ressources nécessaires lors de la vérification d'un modèle. Nous nous intéressons à une modélisation d'un sous ensemble du langage AltaRica , pour lequel une méthode d'abstraction hiérarchique est décrite, ainsi qu'un algorithme efficace permettant la vérification de contre-exemples issus de cette abstraction. La méthode proposée permet d'abstraire chaque composant de la hiérarchie indépendamment malgré la présence de priorités dans le modèle. Finalement l'implémentation de l'algorithme PCegar dans le model checker Mec 5 est présentée ainsi qu'une analyse de benchmarks sur des modèles académiques et un modèle industriel. / This thesis presents an abstraction verification method for AltaRica models. To this end a CEGAR algorithm that prunes away abstract states and therefore uses an underapproximation of the system state space is proposed. The use of an underapproximation of the abstract state space allow to accelerate the algorithm, and reduce the computational resources required by the algorithm. A CEGAR algorithm for a subset of the AltaRica language is also presented. A hierarchical abstractionscheme and an efficient counter-example analysis method are proposed. The abstraction scheme proposed allow to abstract each component independently despite the presence of priorities in the model. Finally, the implementation of our CEGAR with pruning method is present together with benchmarks on academic and industrial models.

L’introduction des nouvelles technologies de l’information et de la communication dans les systèmes automatisés entraîne un accroissement de la complexité des fonctions qu’ils supportent. Cet accroissement de la complexité a un impact sur la sécurité des systèmes. En effet, leurs propriétés ne sont plus réductibles aux propriétés de leurs constituants pris isolément mais émergent d’un réseau d’interactions entre ces constituants qui peut être à l’origine de comportements néfastes et difficiles à prévoir. Notre conviction est que le développement sûr de ces systèmes doit combiner des approches pragmatiques orientées « système », qui tiennent compte du facteur d'échelle réel d'une automatisation pour appréhender le fonctionnement global du système et son architecture, avec des approches plus formelles qui permettent de s’assurer que les propriétés intrinsèques des constituants contribuent efficacement au respect des exigences « système » formulées par les utilisateurs. Le travail présenté dans ce mémoire définit donc une approche méthodologique basée sur le formalisme SysML (System Modeling Language) permettant l’identification, la formalisation et la structuration d’exigences globales relatives à un système, puis leur projection, sous forme de propriétés invariantes, sur une architecture de composants. La vérification des exigences de sécurité, repose alors, d’une part, sur un raffinement prouvé (par theroem proving) des exigences « système » permettant d’établir leur équivalence avec un ensemble de propriétés intrinsèques relatives à chacun des composants, et d’autre part, sur la vérification formelle (par model checking) de ces propriétés intrinsèques. / Introduction of new information and communication technology in automated systems leads to a growth of safety functions complexity. System properties are not limited to components properties, they issued from an interactions network that can introduces bad behaviour. Our conviction is that a safe development of such system must involve system oriented approaches in order to apprehend system global behaviour and architecture and more formal approaches allowing verifying that components properties satisfy end users system requirements We define a methodological approach based on SysML formalism (System Modelling Language) allowing global system requirements identification; formalisation and structuring in order to project these requirements on the system components architecture and so obtain local components properties. Then safety requirements verification is based in one hand on proved refinement (using theorem proving) of system requirements to components properties; and, in the other hand, on the formal verification (using model checking) of these components properties.

Model checking is an automated technique for deciding whether a computer program satisfies a temporal property. Abstraction is the key to scaling model checking to industrial-sized problems, which approximates a large (or infinite) program by a smaller abstract model and lifts the model checking result over the abstract model back to the original program. In this thesis, we study abstraction in model checking based on \emph{exact-approximation}, which allows for verification and refutation of temporal properties within the same abstraction framework. Our work in this thesis is driven by problems from both practical and theoretical aspects of exact-approximation. We first address challenges of effectively applying symmetry reduction to \emph{virtually} symmetric programs. Symmetry reduction can be seen as a \emph{strong} exact-approximation technique, where a property holds on the original program if and only if it holds on the abstract model. In this thesis, we develop an efficient procedure for identifying virtual symmetry in programs. We also explore techniques for combining virtual symmetry with symbolic model checking. Our second study investigates model checking of \emph{recursive} programs. Previously, we have developed a software model checker for non-recursive programs based on exact-approximating predicate abstraction. In this thesis, we extend it to reachability and non-termination analysis of recursive programs. We propose a new program semantics that effectively removes call stacks while preserving reachability and non-termination. By doing this, we reduce recursive analysis to non-recursive one, which allows us to reuse existing abstract analysis in our software model checker to handle recursive programs. A variety of \emph{partial} transition systems have been proposed for construction of abstract models in exact-approximation. Our third study conducts a systematic analysis of them from both semantic and logical points of view. We analyze the connection between semantic and logical consistency of partial transition systems, compare the expressive power of different families of these formalisms, and discuss the precision of model checking over them. Abstraction based on exact-approximation uses a uniform framework to prove correctness and detect errors of computer programs. Our results in this thesis provide better understanding of this approach and extend its applicability in practice.

Model checking is an automated technique for deciding whether a computer program satisfies a temporal property. Abstraction is the key to scaling model checking to industrial-sized problems, which approximates a large (or infinite) program by a smaller abstract model and lifts the model checking result over the abstract model back to the original program. In this thesis, we study abstraction in model checking based on \emph{exact-approximation}, which allows for verification and refutation of temporal properties within the same abstraction framework. Our work in this thesis is driven by problems from both practical and theoretical aspects of exact-approximation. We first address challenges of effectively applying symmetry reduction to \emph{virtually} symmetric programs. Symmetry reduction can be seen as a \emph{strong} exact-approximation technique, where a property holds on the original program if and only if it holds on the abstract model. In this thesis, we develop an efficient procedure for identifying virtual symmetry in programs. We also explore techniques for combining virtual symmetry with symbolic model checking. Our second study investigates model checking of \emph{recursive} programs. Previously, we have developed a software model checker for non-recursive programs based on exact-approximating predicate abstraction. In this thesis, we extend it to reachability and non-termination analysis of recursive programs. We propose a new program semantics that effectively removes call stacks while preserving reachability and non-termination. By doing this, we reduce recursive analysis to non-recursive one, which allows us to reuse existing abstract analysis in our software model checker to handle recursive programs. A variety of \emph{partial} transition systems have been proposed for construction of abstract models in exact-approximation. Our third study conducts a systematic analysis of them from both semantic and logical points of view. We analyze the connection between semantic and logical consistency of partial transition systems, compare the expressive power of different families of these formalisms, and discuss the precision of model checking over them. Abstraction based on exact-approximation uses a uniform framework to prove correctness and detect errors of computer programs. Our results in this thesis provide better understanding of this approach and extend its applicability in practice.