ATVA 2013

In many practical application domains, the software is organized into a set of threads, whose activation is exclusive and controlled by a cooperative scheduling policy: threads execute, without any interruption, until they either terminate or yield the control explicitly to the scheduler.

The formal verification of such software poses significant challenges. On the one side, each thread may have infinite state space, that might require some abstraction. On the other side, the scheduling policy is often important for correctness, and an approach based on abstracting the scheduler may result in loss of precision and false positives. Unfortunately, the translation of the problem into a purely sequential software model checking problem turns out to be highly inefficient for the available technologies.

We discuss a software model checking technique that exploits the intrinsic structure of these programs. Each thread is translated into a separate sequential program and explored symbolically with lazy abstraction, while the overall verification is orchestrated by the direct execution of the scheduler. The approach is optimized by filtering the exploration of the scheduler with the integration of partial-order reduction. The technique, called ESST (Explicit Scheduler, Symbolic Threads) has been implemented and experimentally evaluated on a significant set of benchmarks. The results demonstrate that ESST technique is way more effective than software model checking applied to the sequentialized programs, and that partial-order reduction can lead to further performance improvements.

Probabilistic model checking is an automated technique to verify whether a probabilistic system, e.g. a distributed network protocol which can exhibit failures, satisfies a temporal logic property, for example, the minimum probability of the network recovering from a fault in a given time period is above 0.98. One can also generate, given a model and a temporal property, a strategy for controlling the system in order to achieve or optimise the property, but this aspect has received less attention to date. In this paper, we give an overview of methods for automated verification and strategy synthesis, focusing on Markov decision process models and temporal logics PCTL and LTL. We also describe how to apply multi-objective model checking to investigate trade-offs between the properties. We illustrate these techniques by means of several case studies analysed in the PRISM model checker. The paper concludes with a summary of future challenges in this area.

The reachability problem for Petri nets is a central problem of net theory. The problem is known to be decidable by inductive invariants definable in the Presburger arithmetic. When the reachability set is definable in the Presburger arithmetic, the existence of such an inductive invariant is immediate. However, in this case, the computation of a Presburger formula denoting the reachability set is an open problem. Recently this problem got closed by proving that if the reachability set of a Petri net is definable in the Presburger arithmetic, then the Petri net is flatable, i.e. its reachability set can be obtained by runs labeled by words in a bounded language. As a direct consequence, classical algorithms based on acceleration techniques effectively compute a formula in the Presburger arithmetic denoting the reachability set. In this presentation, the framework of verification of infinite-state systems based on acceleration techniques is recalled. We also explain the completeness of this method on the computation of Presburger formulas denoting the reachability sets of Petri nets.

Hybrid automata are a widely used framework to model complex critical systems, where continuous physical dynamics are combined with discrete transitions. Application areas include automotive, railway, aerospace, and industrial production. The expressive power of Satisfiability Modulo Theories (SMT) solvers can be used to symbolically model networks of hybrid automata, using formulas in the theory of reals. In this tutorial, we survey the state-of-the-art in SMT-based verification for hybrid systems. We show how SAT-based techniques such as bounded model checking, k-induction, predicate abstraction, and IC3, can be naturally lifted to the SMT case. The expressive power of the SMT framework allows us to exploit a local time semantics, where the timescales of the automata in the network are synchronized upon shared events. The approach fully leverages the advanced features of modern SMT solvers, such as incrementality, unsatisfiable core extraction, and interpolation. We then concentrate on the problem of scenario-based verification, i.e. checking if a network of hybrid automata accepts some desired interactions among the components, expressed as Message Sequence Charts (MSCs). We conclude by investigating the problem of requirements analysis for hybrid systems.

Probabilistic model checking is an automated method for establishing the correctness of probabilistic system models against temporal logic specifications. The techniques have been implemented in the probabilistic model checker PRISM (www.prismmodelchecker.org) and applied to analyse and detect flaws in several real-world systems, across a wide range of application domains. In this tutorial, we give a brief overview of probabilistic model checking, focusing on the model of Markov decision processes, and briefly summarise recent developments of the tool, including parametric models, multi-objective model checking, strategy generation and verification for stochastic games.

Systems equipped with counters are central when modeling distributed protocols, programs with recursive parallel threads, programs with pointers, broadcast protocols, databases, etc. When it comes to model-checking counter systems and their variants, the main results are that verification is undecidable when zero-tests are allowed, while several problems can be decided when zero-tests are forbidden—one speaks of VASS, for "vector addition systems with states", or equivalently "Petri nets". In the case of Petri net, reachability was shown decidable in 1982 and the reachability problem for Petri net and related decidable problems on subclasses of counter systems are pivot problems not only for the verification of infinite-state systems but also for problems appearing in very active research areas related to various logics and automata for data words/trees. Hence, the design of efficient algorithms for the reachability problem for VASS may have a great impact, not only in the realm of formal verification. It is however a very difficult problem. Therefore, improving the computational cost for solving the reachability problem for Petri nets would also improve the complexity of the formal verification of numerous classes of infinite-state systems.

Strikingly, the decision algorithm for Petri net reachability has never been implemented. This is because of its high complexity, both conceptual (the algorithm is very hard to understand and to describe) and computational (it is assumed that the complexity of the algorithm is not primitive-recursive). The general problem is known to be decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition (KLMTS decomposition). Recently from this decomposition, we deduced that a final configuration is not reachable from an initial one if and only if there exists a Presburger inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Presburger formula denotes an inductive invariant, we deduce from this result that there exist checkable certificates of non-reachability in the Presburger arithmetic. In particular, there exists a simple algorithm for deciding the general Petri net reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas. In this presentation we provide a simple proof of the Petri net reachability problem that is not based on the KLMST decomposition. The proof is based on the notion of production relations, inspired from Hauschildt, that directly proves the existence of Presburger inductive invariants.