Abstract (click to open/close)

Counterexamples are a highly important feature of the model checking process. In contrast to, e. g., digital circuits where counterexamples typically consist of a single path leading to a critical state of the system, in the probabilistic setting, counterexamples may consist of a large number of paths. In order to be able to handle large systems and to use the capabilities of modern SAT-solvers, bounded model checking (BMC) for discrete-time Markov chains was established. In this paper we introduce the usage of SMT-solving over the reals for the BMC procedure. SMT-solving, extending SAT with theories, leads in this context on the one hand to a convenient way to express conditions on the probability of certain paths and on the other hand to handle Markov Reward models. The former can be used to find paths with high probability first. This leads to more compact counterexamples. We report on some experiments, which show promising results.

Subproject(s): S3

Abstract (click to open/close)

We address the complete design flow from specification models of new automotive functions captured in Matlab-Simulink to their distributed execution on hierarchical bus-based electronic architectures hosting the release of already deployed automotive functions. We propose an automated design space exploration process resulting in a cost-optimized extension of the existing target hardware and an allocation of balanced task structures automatically derived from the specification model on this modified target hardware which is sufficient to guarantee both system-level timing requirements and deadlines extracted from the Matlab-Simulink specification model.

Subproject(s): R2

Abstract (click to open/close)

Real-time scheduling theory is a powerful technique for efficient analysis of system behaviour. Task Networks as common formalisms for scheduling analysis however often lack expressive power to model functional behaviour like for example different modes of operation. Research focuses on combining different formalisms to raise the expressiveness while maintaining efficient real-time analysis methods. There are rare approaches to extend task network formalisms itself. Though, this would allow a tight integration of scheduling analysis and other verification techniques. Real-time scheduling analysis however heavily relies on decidability of boundedness for executions, and this is not necessarily ensured for more complex formalisms. We discuss such an extended formalism able to model complex real-time systems, and we show that boundedness is still decidable here.

Subproject(s): R2

Abstract (click to open/close)

We propose an improved symbolic algorithm for the verification of linear hybrid automata with large discrete state spaces (where an explicit representation of discrete states is difficult). Here both the discrete part and the continuous part of the hybrid state space are represented by one symbolic representation called LinAIGs. LinAIGs represent (possibly non-convex) polyhedra extended by boolean variables. Key components of our method for state space traversal are redundancy elimination and constraint minimization: Redundancy elimination eliminates so-called redundant linear constraints from LinAIG representations by a suitable exploitation of the capabilities of SMT (Satisfiability Modulo Theories) solvers. Constraint minimization optimizes polyhedra by exploiting the fact that states already reached in previous steps can be interpreted as 'don't cares' in the current step. Experimental results (including comparisons to the state-of-the-art model checkers PHAVer and RED) demonstrate the advantages of our approach.

Subproject(s): H3

Abstract (click to open/close)

This paper identifies an industrially relevant class of linear hybrid automata (LHA) called reasonable LHA for which parametric verification of safety properties with exhaustive entry conditions can be verified in polynomial time and timebounded reachability with exhaustive entry conditions can be decided in nondeterministic polynomial time for nonparametric verification and in exponential time for parametric verification. Deciding whether an LHA is reasonable is shown to be decidable in polynomial time.

Subproject(s): H3

Abstract (click to open/close)

Dealing with the interplay of randomness and continuous time is important for the formal verification of many real systems. Considering both facets is especially important for wireless sensor networks, distributed control applications, and many other systems of growing importance. An important traditional design and verification goal for such systems is to ensure that unsafe states can never be reached. In the stochastic setting, this translates to the question whether the probability to reach unsafe states remains tolerable. In this paper, we consider stochastic hybrid systems where the continuous-time behaviour is given by differential equations, as for usual hybrid systems, but the targets of discrete jumps are chosen by probability distributions. These distributions may be general measures on state sets. Also non-determinism is supported, and the latter is exploited in an abstraction and evaluation method that establishes safe upper bounds on reachability probabilities. To arrive there requires us to solve semantic intricacies as well as practical problems. In particular, we show that measurability of a complete system follows from the measurability of its constituent parts. On the practical side, we enhance tool support to work effectively on such general models. Experimental evidence is provided demonstrating the applicability of our approach on three case studies, tackled using a prototypical implementation.

Subproject(s): H4

Abstract (click to open/close)

Die vorliegende Arbeit behandelt die Berechnung Craigscher Interpolanten für beliebige boolesche Kombinationen linearer und nichtlinearer Gleichungen, einschließlich transzendenter Funktionen wie sin (x) und cos (x). Craigsche Interpolanten sind in der computergestützten Verifikation weit verbreitet und können für viele verschiedene Theorien berechnet werden, zum Beispiel: Aussagenlogik, lineare Arithmetik über rationale Zahlen sowie die Theorie mit uninterpretierten Funktionsymbolen. Nach bestem Wissen berechnen alle uns bekannten Interpolationsprogramme Craigsche Interpolanten für entscheidbare Theorien. In dieser Arbeit stellen wir einen Ansatz vor, der für eine im Allgemeinem nicht entscheidbare Theorie Craigsche Interpolanten berechnen kann. Wir erlauben neben linearen und nichtlinearen Gleichungen auch transzendente Funktionen. Solche Formeln entstehen bei der Analyse und Verifikation hybrider Systeme. Der in dieser Arbeit vorgestellte Ansatz wurde mithilfe des Sat-Modulo-Theorie Solvers iSAT implementiert. Erste Ergebnisse zeigen, dass Craigsche Interpolanten bei der Verifikation solcher Systeme erfolgreich eingesetzt werden können.

Keywords: iSAT interpolation proof interval arithmetic
Subproject(s): H1/2

Abstract (click to open/close)

Directed model checking is a well-established technique for detecting error states in concurrent systems efficiently. As error traces are important for debugging purposes, it is preferable to find as short error traces as possible. A wide spread method to find provably shortest error traces is to apply the A* search algorithm with distance heuristics that never overestimate the real error distance. An important class of such distance estimators is the class of pattern database heuristics, which are built on abstractions of the system under consideration. In this paper, we propose a systematic approach for the construction of pattern database heuristics. We formally define a concept to measure the accuracy of abstractions. Based on this technique, we address the challenge of finding abstractions that are succinct on the one hand, and accurate to produce informed pattern databases on the other hand. We evaluate our approach on large and complex industrial problems. The experiments show that the resulting distance heuristic impressively advances the state of the art.

Subproject(s): R3

Subproject(s): S1

Abstract (click to open/close)

Verification of real-time systems -- e.g. communication protocols or embedded controllers -- is an important task. One method to detect errors is called bounded model checking (BMC). In BMC a system is iteratively unfolded and then transformed into a satisfiability problem. If an appropriate solver finds the k-th instance to be satisfiable, a counterexample for a given safety property has been found. In this paper, we present a novel approach to apply BMC to networks of timed automata (i.e. a system of several interacting subautomata) where parts of the network are unspecified (so-called blackboxes). Here, we would like to answer the question of unrealizability, that is, is there a path of a certain length violating a safety property regardless of the implementation of the blackboxes. Focusing on two prevalent communication models for networks of interacting timed automata, we introduce two methods to solve these types of BMC problems. The first is based on fixed transitions, which in some cases is too coarse of an abstraction. In the second approach we prove unrealizability by introducing universal quantification, yielding more advanced quantified SAT-Modulo-Theory formulas.

Subproject(s): S1

Abstract (click to open/close)

Self-stabilizing systems, intended to run for a long time, commonly have to cope with transient faults during their mission. We model the behavior of a distributed self-stabilizing system under such a fault model as a Markov chain. Adding fault detection to a self-correcting non-masking fault tolerant system is required to progress from non-masking systems towards their masking fault tolerant functional equivalents. We introduce a novel measure, called limiting window availability (LWA) and apply it on self-stabilizing systems in order to quantify the probability of (masked) stabilization against the time that is needed for stabilization. We show how to calculate LWA based on Markov chains: first, by a straightforward Markov chain modeling and second, by using a suitable abstraction resulting in a space-reduced Markov chain. The proposed abstraction can in particular be applied to spot fault tolerance bottlenecks in the system design.

Subproject(s): S3

Abstract (click to open/close)

In this paper we present a method for integrating two complementary solving techniques for QBF formulas, i. e. variable elimination based on an AIG-framework and search with DPLL based solving. We develop a sophisticated mechanism for coupling these techniques, enabling the transfer of partial results from the variable elimination part to the search part. This includes the definition of heuristics to (1) determine appropriate points in time to snapshot the current partial result during variable elimination (by estimating its quality) and (2) switch from variable elimination to search-based methods (applied to the best known snapshot) when the progress of variable elimination is supposed to be too slow or when representation sizes grow too fast. We will show in the experimental section that our combined approach is clearly superior to both individual methods run in a stand-alone manner. Moreover, our combined approach significantly outperforms all other state-of-the-art solvers.

Subproject(s): S1

Abstract (click to open/close)

The stochastic Boolean satisfiability (SSAT) problem has been introduced by Papadimitriou in 1985 when adding a probabilistic model of uncertainty to propositional satisfiability through randomized quantification. SSAT has many applications, among them bounded model checking (BMC) of symbolically represented Markov decision processes. This paper identifies a notion of Craig interpolant for the SSAT framework and develops an algorithm for computing such interpolants based on SSAT resolution. As a potential application, we address the use of interpolation in SSAT-based BMC, turning the falsification procedure into a verification approach for probabilistic safety properties.

Subproject(s): H1/2,H4

Abstract (click to open/close)

The stochastic Boolean satisfiability (SSAT) problem has been introduced by Papadimitriou in 1985 when adding a probabilistic model of uncertainty to propositional satisfiability through randomized quantification. SSAT has many applications, among them bounded model checking (BMC) of symbolically represented Markov decision processes. This paper identifies a notion of Craig interpolant for the SSAT framework and develops an algorithm for computing such interpolants based on SSAT resolution. As a potential application, we address the use of interpolation in SSAT-based BMC, turning the falsification procedure into a verification approach for probabilistic safety properties.

Subproject(s): H1/2,H4

Abstract (click to open/close)

In previous publications, the authors have introduced the notion of stochastic satisfiability modulo theories (SSMT) and the corresponding SiSAT solving algorithm, which provide a symbolic method for the reachability analysis of probabilistic hybrid systems. SSMT extends satisfiability modulo theories (SMT) with randomized (or stochastic), existential, and universal quantification, as known from stochastic propositional satisfiability. In this paper, we extend the SSMT-based procedures to the symbolic analysis of concurrent probabilistic hybrid systems. After formally introducing the computational model, we provide a mechanized translation scheme to encode probabilistic bounded reachability problems of concurrent probabilistic hybrid automata as linearly sized SSMT formulae, which in turn can be solved by the SiSAT tool. We furthermore propose an algorithmic enhancement which tailors SiSAT to probabilistic bounded reachability problems by caching and reusing solutions obtained on bounded reachability problems of smaller depth. An essential part of this article is devoted to a case study from the networked automation systems domain. We explain in detail the formal model in terms of concurrent probabilistic automata, its encoding into the SiSAT modeling language, and finally the automated quantitative analysis.

Keywords: Concurrent probabilistic hybrid systems, probabilistic logic, constraint satisfaction problems, problem solvers, automatic verification
Subproject(s): H1/2,H4

Abstract (click to open/close)

Markow-Ketten mit diskreter und kontinuierlicher Zeit sowie interaktive Markow-Ketten sind weitverbreitete Modellklassen zur Analyse von stochastischen Systemen. Ein grundlegendes Problem bei ihrer Analyse ist die Anzahl der Zustände. Diese wächst nämlich im Allgemeinen exponentiell in der Größe des zugehörigen Highlevel-Modells.

Wir entwickeln in dieser Arbeit zwei Methoden, mit denen dieses Problem gelöst werden kann. Die erste besteht darin, zu jedem System dasjenige zu berechnen, das aus einer minimalen Anzahl von Zuständen besteht und das dasselbe beobachtbare Verhalten wie das ursprüngliche System aufweist. Danach kann die Analyse mit bekannten Algorithmen auf dem minimierten System durchgeführt werden. Abhängig von der Definition, welches Verhalten des Systems beobachtbar ist, erhalten wir verschiedene minimale Systeme. Unser Algorithmus ist in der Lage, eine ganze Reihe von Minimierungskriterien, die in der Literatur von Bedeutung sind, und Systemtypen zu berücksichtigen. Er arbeitet mit symbolischen Datenstrukturen und darauf angepassten Operationen, deren Laufzeit nur von der Größe der Darstellung abhängt. Für viele praktisch relevante Systeme ist diese um Größenordnungen kleiner als die Größe des dargestellten Systems. Experimentelle Ergebnisse belegen die Effzienz unseres Verfahrens.

Die andere Methode, mit großen Zustandsräumen umzugehen, ist, symbolische Algorithmen zur Analyse zu entwickeln, die direkt auf große Systemen anwendbar sind. Für die Fehlersuche in Schaltkreisen wird eine Methode namens Bounded Model Checking verwendet, die inzwischen auch industriell sehr erfolgreich eingesetzt wird. Wir zeigen, wie Bounded Model Checking zur Berechnung von Gegenbeispielen für Markow-Ketten eingesetzt werden kann, wenn diese eine vorgegebene Sicherheitseigenschaft verletzen. Durch eine Reihe von Optimierungen gelingt es uns, sowohl die Laufzeit zu reduzieren als auch die Größe der Gegenbeispiele zu verringern. Das Resultat ist ein Verfahren, das deutlich größere Systeme als die bisher verfügbaren expliziten Methoden handhaben kann.

Subproject(s): S3

Abstract (click to open/close)

Discrete-Time Markov Chains (DTMCs) are a widely-used formalism to model probabilistic systems. On the one hand, available tools like textsc Prism or textsc Mrmc offer efficient model checking algorithms and thus support the verification of DTMCs. However, these algorithms do not provide any diagnostic information in the form of counterexamples, which are highly important for the correction of erroneous systems. On the other hand, there exist several approaches to generate counterexamples for DTMCs, but all these approaches require the model checking result for completeness.

In this paper we introduce a model checking algorithm for DTMCs that also supports the generation of counterexamples. Our algorithm, based on the detection and abstraction of strongly connected components, offers abstract counterexamples, which can be interactively refined by the user.

Subproject(s): S3

Abstract (click to open/close)

Hard real-time systems require tasks to finish in time. To guarantee the timeliness of such a system, static timing analyses derive upper bounds on the worst-case execution time of tasks. There are two types of timing analyses: numeric and parametric ones. A numeric analysis derives a numeric timing bound and, to this end, assumes all information such as loop bounds to be given a priori. If these bounds are unknown during analysis time, a parametric analysis can compute a timing formula parametric in these variables. A performance bottleneck of timing analyses, numeric and especially parametric, can be the so-called path analysis, which determines the path in the analyzed task with the longest execution time bound. In this paper, we present a new approach to the path analysis. This approach exploits the rather regular structure of software for hard real-time and safety-critical systems. As we show in the evaluation of this paper, we strongly improve upon former techniques in terms of precision and runtime in the parametric case. Even in the numeric case, our approach matches up to state-of-the-art techniques and may be an alternative to commercial tools employed for path analysis.

Subproject(s): R2

Abstract (click to open/close)

We present a partial solution to the TTC2010 topology analysis case study. We pick a small part of the merge protocol, namely the part where cars join a leader to form a platoon. Using abstract interpretation, we compute an approximation of the arising topologies, without limiting the number of cars.

Subproject(s): S2

Abstract (click to open/close)

We propose a case study for the Transformation Tool Contest 2010 that concerns dynamic communication systems (DCS). DCS are systems of autonomous processes that interact to achieve their goals. For this purpose, the processes exchange messages with each other. In contrast to distributed algorithms, the number of processes of the system is unbounded. The specific dynamic communication systems we want to investigate are so-called platoons. Platoons are groups of cars that drive on a highway with constant speed and constant distance to conserve energy. To form such platoons, each car follows the so-called merge protocol, which guides its local behaviour. We are interested in properties of the communication topologies that may emerge in this platoon scenario. Hence, we ask you to analyze a graph transformation system that generates the possible topologies of the merge protocol. The goal is to do this with as many processes as possible. The case study aims to improve understanding of how useful existing tools are for state space exploration and topology analysis.

Subproject(s): S2

Abstract (click to open/close)

We present a method to enhance the power of a given reachability analysis engine for hybrid systems. The method works by a new form of composition of reachability analyses, each on a different relaxation of the input hybrid system. We present preliminary experiments that indicate its practical potential for checking safety and stability.

Subproject(s): H3,H4

Abstract (click to open/close)

The landmark cut heuristic is perhaps the strongest known polytime admissible approximation of the optimal delete relaxation heuristic h^+. Equipped with this heuristic, a best-first search was able to optimally solve 40% more benchmark problems than the winners of the sequential optimization track of IPC 2008. We show that this heuristic can be understood as a simple relaxation of a hitting set problem, and that stronger heuristics can be obtained by considering stronger relaxations. Based on these findings, we propose a simple polytime method for obtaining heuristics stronger than landmark cut, and evaluate them over benchmark problems. We also show that hitting sets can be used to characterize h^+ and thus provide a fresh and novel insight for better comprehension of the delete relaxation.

Subproject(s): S1

Abstract (click to open/close)

For checking the temporal behaviour of embedded systems, real-time scheduling analysis based on abstract, formal models is a well-established method. A major difficulty for such analytical models in practical use-cases is the non-trivial representation of a real implementation model. To overcome this limitation we propose a formal mapping of a concurrent, objectoriented, executable implementation model with explicit shared resources to a real-time task network with functional extensions. The mapping starts from a C++ subset and maps the functional behaviour based on externally observable synchronisation events. The proposed mapping allows to check the implementation model against functional and temporal requirements, like local and end-to-end deadlines.

Subproject(s): R2

Abstract (click to open/close)

We develop an algorithm to compute timed reachability probabilities for distributed models which are both probabilistic and nondeterministic. To obtain realistic results we consider the recently introduced class of (strongly) distributed schedulers, for which no analysis techniques are known.Our algorithm is based on reformulating the nondeterministic models as parametric ones, by interpreting scheduler decisions as parameters. We then apply the PARAM tool to extract the reachability probability as a polynomial function, which we optimize using nonlinear programming.

Subproject(s): S3

Abstract (click to open/close)

We develop an algorithm to compute timed reachability probabilities for distributed models which are both probabilistic and nondeterministic. To obtain realistic results we consider the recently introduced class of (strongly) distributed schedulers, for which no analysis techniques are known.

Subproject(s): S3

Abstract (click to open/close)

Interpolation has proven highly effective in program analysis and verification, e. g., to derive invariants or new abstractions. While interpolation for quantifier free formulae is understood quite well, it turns out to be challenging in the presence of quantifiers. We present in this paper modifications to instantiation based SMT-solvers and to McMillan's interpolation algorithm in order to compute quantified interpolants.

Subproject(s): R1

Abstract (click to open/close)

Compositional modeling is a powerful way of expressing the behavior of a complex system through the interaction of its components. Analysis of compositional models is difficult because of the state space explosion. One solution is compositional aggregation where composition and aggregation steps are intertwined. This approach has proven particularly useful in the area of compositional performance and dependability modelling. However, one open question remains: in which order should the models be composed, a question that is especially important for massively compositional models derived automatically from higher level descriptions. Finding the optimal composition ordering is generally infeasible, so heuristics are necessary to find good orderings. In this paper we present a comparative study of compositional aggregation algorithms which harvest and refine heuristics originating from Tai and Koppol. The heuristics take into account the interaction between components, the size of the component models and uses early elimination of bad composition orders to dramatically decrease computation time. We present an implementation of the algorithms and study its effectiveness by applying it to case studies from different application areas.

Subproject(s): S3

Abstract (click to open/close)

This paper investigates quantitative dependability metrics for distributed algorithms operating in the presence of sporadic or frequently occurring faults. In particular, we investigate necessary revisions of traditional fairness assumptions in order to arrive at useful metrics, without adding hidden assumptions that may obfuscate their validity. We formulate distributed algorithms as Markov decision processes to incorporate both probabilistic faults and non-determinism arising from the distributed setting. We especially discuss the notions of bounded fairness and near-round-robin schedulers, which appear particularly suited for distributed algorithms running on nearly symmetric infrastructure, as it is common for sensor network applications. We further develop methods to incorporate this fairness notion in the quantitative model checking of distributed algorithms. Finally, we apply our methodology to several case studies to provide a first experimental insight into its applicability.

Subproject(s): S3

Abstract (click to open/close)

We propose a library based incremental design methodology for constructing hybrid controllers from a component library of models of hybrid controllers, such that global safety and stability properties are preserved. To this end, we propose hybrid interface specifications of components characterizing plant regions for which safety and stability properties are guaranteed, as well as exception mechanisms allowing safe and stability-preserving transfer of control whenever the plant evolves towards the boundary of controllable dynamics. We then propose a composition operator for constructing hybrid automata from a library of such pre-characterized components supported by compositional and automatable proofs of hybrid interface specifications.

Subproject(s): H3

Abstract (click to open/close)

The complexity of designing self-stabilizing systems is often compounded by the assumptions about the underlying schedulers. This paper presents a method to transform a self-stabilizing algorithm working under a given arbitrary, but potentially very restrictive, scheduler to a self-stabilizing algorithm under any weakly fair scheduler. The method presented here implements a emph progress monitor by exploiting the knowledge of a ranking function --used for proving convergence under the original scheduler-- to carry out the transformation.

Subproject(s): H4

Abstract (click to open/close)

Systems and protocols combining concurrency and infinite state space occur quite often in practice, but are very difficult to verify automatically. At the same time, if the system is correct, it is desirable for a verifier to obtain not a simple "yes" answer, but some independently checkable certificate of correctness. We present SLAB --- the first certifying model checker for infinite-state concurrent systems. The tool uses a procedure that interleaves automatic abstraction refinement using Craig interpolation with slicing, which removes irrelevant states and transitions from the abstraction. Given a transition system and a safety property to check, SLAB either finds a counterexample or produces a certificate of system correctness in the form of inductive verification diagram.

Subproject(s): R1,S1

Abstract (click to open/close)

In this talk, we present our approach to perform bounded model checking (BMC) of hybrid discrete continuous systems using constraint solving techniques. The BMC problem can be expressed by a Boolean combination of arithmetic constraints and ordinary differential equations (ODEs). While the Boolean, integer, and real-valued variables represent the state of the hybrid system, the constraint system describes traces characterized by their initial states, a transition relation connecting subsequent states by continuous flows or discrete jumps, and a target state whose reachability is to be analyzed. The reachability problem of the hybrid system therefore becomes a satisfiability problem of this type of formula. We extend our constraint solving algorithm iSAT to also handle the ODEs occuring in these formulae by using safe enclosures of the ODEs solution trajectories thereby coupling the structure of the DPLL procedure, which is used successfully in propositional satisfiability solving, with interval methods for arithmetic constraints and safe enclosure methods for the solutions of initial value problems. Our current work is focused (1) on exchanging our prototypical enclosure mechanism with Ned Nedialkov's VNODE-LP in order to obtain such enclosures more efficiently and (2) on storing once-deduced knowledge and potentially further information available on the solution trajectories persistently in the constraint system to avoid costly enclosures in the first place. Keywords: Hybrid discrete continuous systems, automatic verification, satisfiability modulo theories, ordinary differential equations Joint work of: Eggers, Andreas; Fr�nzle, Martin; Herde, Christian

Subproject(s): H1/2

Abstract (click to open/close)

We show how deterministic Buechi automata can be fully minimised by reduction to the satisfiability (SAT) problem, yielding the first automated method for this task. Size reduction of such w-automata is an important step in probabilistic model checking as well as synthesis of finite-state systems. Our experiments demonstrate that state-of-theart SAT solvers are capable of solving the resulting satisfiability problem instances quickly, making the approach presented valuable in practice.

Abstract (click to open/close)

Emptiness checking of omega-automata is a fundamental part of the automata-theoretic toolbox and is frequently applied in many applications, most notably verification of reactive systems. In this particular application, the capability to extract accepted words or alternatively accepting runs in case of non-emptiness is particularly useful, as these have a diagnostic value. However, non-optimised such words or runs can become huge, limiting their usability in practice, thus solutions with a small representation should be preferred. In this paper, we review the known results on obtaining these and complete the complexity landscape for all commonly used automaton types. We also prove upper and lower bounds on the approximation hardness of these problems.

Subproject(s): S1

Abstract (click to open/close)

Synthesis of finite state systems from full linear time temporal logic (LTL) specifications is gaining more and more attention as several recent achievements have significantly improved its practical applicability. Many works in this area are based on the Safraless synthesis approach. Here, the computation is usually performed either in an explicit way or using symbolic data structures other than binary decision diagrams (BDDs). In this paper, we close this gap and consider Safraless synthesis using BDDs as state space representation. The key to this combination is the application of novel optimisation techniques which decrease the number of state bits in such a representation significantly. We evaluate our approach on several practical benchmarks, including a new load balancing case study. Our experiments show an improvement of several orders of magnitude over previous approaches.

Subproject(s): S1

Abstract (click to open/close)

Explicit-state model checkers like SPIN, which verify systems against properties stated in linear-time temporal logic (LTL), rely on efficient LTL-to-Buechi translators. A difficult design decision in such constructions is to trade time spent on minimizing the Buechi automaton versus time spent on model checking against an unnecessarily large automaton. Standard reduction methods like simulation quotienting are fast but often miss optimization opportunities. We propose a new technique that achieves significant further reductions when more time can be invested in the minimization of the automaton. The additional effort is often justified, for example, when the properties are known in advance, or when the same property is used in multiple model checking runs. We use a modified SAT solver to perform bounded language inclusion checks on partial solutions. SAT solving allows us to prune large parts of the search space for smaller automata already in the early solving stages. The bound allows us to fine-tune the algorithm to run in limited time. Our experimental results show that, on standard LTL-to-Buechi benchmarks, our prototype implementation achieves a significant further size reduction on automata obtained by the best currently available LTL-to-Buechi translators.

Subproject(s): S1

Abstract (click to open/close)

We present constraint matrix diagrams (CMDs), a novel data structure for the fully symbolic reachability analysis of timed automata. CMDs combine matrix-based and diagram-based state space representations generalizing the concepts of difference bound matrices (DBMs), clock difference diagrams (CDDs), and clock restriction diagrams (CRDs). The key idea is to represent convex parts of the state space as (partial) DBMs which are, in turn, organized in a CDD/CRD-like ordered and reduced diagram. The location information is incorporated as a special Boolean constraint in the matrices. We describe all CMD operations needed for the construction of the transition relation and the reachability fixed point computation. Based on a prototype implementation, we compare our technique with the timed model checkers RED and Uppaal, and furthermore investigate the impact of two different reduced forms on the time and space consumption.

Subproject(s): S1

Abstract (click to open/close)

The success of industrial-scale model checkers such as Uppaal or NuSMV relies on the efficiency of their respective symbolic state space representations. While difference bound matrices (DBMs) are effective for representing sets of clock values, binary decision diagrams (BDDs) can efficiently represent huge discrete state sets. In this paper, we introduce a simple general framework for combining both data structures, enabling a joint symbolic representation of the timed state sets in the reachability fixed point construction. In contrast to other approaches, our technique is neither sensitive to the magnitude of the clocks nor suffers from intricate interdependencies between clock constraints and the location information. Especially in the analysis of models with only few clocks, large constants, and a huge discrete state space (such as, e.g., data-intensive communication protocols), our technique turns out to be highly effective. Additionally, our framework allows to employ existing highly-optimized implementations for DBMs and BDDs without modifications. Using a prototype implementation, we are able to verify a central correctness property of the coding/decoding part of the FlexRay communication protocol taking an unreliable physical layer into account.

Subproject(s): S1

Abstract (click to open/close)

We present a general approach to combine symbolic state space representations for the discrete and continuous parts in the synthesis of winning strategies for timed reachability games. The combination is based on abstraction refinement where discrete symbolic techniques are used to produce a sequence of abstract timed game automata. After each refinement step, the resulting abstraction is used for computing an under- and an over-approximation of the timed winning states. The key idea is to identify large relevant and irrelevant parts of the precise weakest winning strategy already on coarse, and therefore simple, abstractions. If neither the existence nor nonexistence of a winning strategy can be established in the approximations, we use them to guide the refinement process. Based on a prototype that combines binary decision diagrams and difference bound matrices, we experimentally evaluate the technique on standard benchmarks from timed controller synthesis. The results clearly demonstrate the potential of the new approach concerning running time and memory consumption compared to the classical on-the-fly algorithm implemented in UPPAAL-Tiga.

Subproject(s): S1,R3

Abstract (click to open/close)

We discuss conceptional and foundational aspects of Markov automata [22]. We place this model in the context of continuous- and discrete-time Markov chains, probabilistic automata and interactive Markov chains, and provide insight into the parallel execution of such models. We further give a detailled account of the concept of relations on distributions, and discuss how this can generalise known notions of weak simulation and bisimulation, such as to fuse sequences of internal transitions.

Subproject(s): S3

Abstract (click to open/close)

We develop a compositional behavioural model that integrates a variation of probabilistic automata into a conservative extension of interactive Markov chains. The model is rich enough to embody the semantics of generalised stochastic Petri nets. We define strong and weak bisimulations and discuss their compositionality properties. Weak bisimulation is partly oblivious to the probabilistic branching structure, in order to reflect some natural equalities in this spectrum of models. As a result, the standard way to associate a stochastic process to a generalised stochastic Petri net can be proven sound with respect to weak bisimulation.

Subproject(s): S3

Abstract (click to open/close)

We develop a compositional behavioural model that integrates a variation of probabilistic automata into a conservative extension of interactive Markov chains. The model is rich enough to embody the semantics of generalised stochastic Petri nets. We define strong and weak bisimulations and discuss their compositionality properties. Weak bisimulation is partly oblivious to the probabilistic branching structure, in order to reflect some natural equalities in this spectrum of models. As a result, the standard way to associate a stochastic process to a generalised stochastic Petri net can be proven sound with respect to weak bisimulation.

Subproject(s): S3

Abstract (click to open/close)

We consider the stochastic variant of the Canadian Traveler's Problem, a path planning problem where adverse weather can cause some roads to be untraversable. The agent does not initially know which roads can be used. However, it knows a probability distribution for the weather, and it can observe the status of roads incident to its location. The objective is to find a policy with low expected travel cost. We introduce and compare several algorithms for the stochastic CTP. Unlike the optimistic approach most commonly considered in the literature, the new approaches we propose take uncertainty into account explicitly. We show that this property enables them to generate policies of much higher quality than the optimistic one, both theoretically and experimentally.

Subproject(s): S1

Subproject(s): S1

Abstract (click to open/close)

We introduce a conceptual approach to decompose real-time systems, speci�ed by integrated formalisms: instead of showing safety of a system directly, one proves that it is an instance of a Veri�cation Architecture, a safe behavioural protocol with unknowns and local real-time assumptions. We examine how different veri�cation techniques can be combined in a uniform framework to reason about protocols, assumptions, and instantiations of protocols. The protocols are speci�ed in CSP, extended by data and unknown processes with local assumptions in a real-time logic. To prove desired properties, the CSP dialect is embedded into dynamic logic and a sequent calculus is presented. Further, we analyse the instantiation of protocols by combined speci�cations, here illustrated by CSP-OZ-DC. Using an example, we show that this approach helps us verify speci�cations that are too complex for direct veri�cation.

Subproject(s): R1

Abstract (click to open/close)

We introduce a conceptual approach to decompose real-time systems, specified by integrated formalisms: instead of showing safety of a system directly, one proves that it is an instance of a Verification Architecture, a safe behavioural protocol with unknowns and local real-time assumptions. We examine how different verification techniques can be combined in a uniform framework to reason about protocols, assumptions, and instantiations of protocols. The protocols are specified in CSP, extended by data and unknown processes with local assumptions in a real-time logic. To prove desired properties, the CSP dialect is embedded into dynamic logic and a sequent calculus is presented. Further, we analyse the instantiation of protocols by combined specifications, here illustrated by CSP-OZ-DC. Using an example, we show that this approach helps us verify specifications that are too complex for direct verification.

Subproject(s): R1

Abstract (click to open/close)

The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.

Subproject(s): R1

Abstract (click to open/close)

The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. (i) For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. (ii) At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. (iii) At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.

Subproject(s): R1,H3

Abstract (click to open/close)

This paper discusses the analysis of first-order probabilistic timed automata (FPTA) by a combination of hierarchic first-order superposition-based theorem proving and probabilistic model checking. We develop the overall semantics of FPTAs and prove soundness and completeness of our method for reachability properties. Basically, we decompose FPTAs into their time plus first-order logic aspects on the one hand, and their probabilistic aspects on the other hand. Then we exploit the time plus first-order behavior by hierarchic superposition over linear arithmetic. The result of this analysis is the basis for the construction of a reachability equivalent (to the original FPTA) probabilistic timed automaton to which probabilistic model checking is finally applied. The hierarchic superposition calculus required for the analysis is sound and complete on the first-order formulas generated from FPTAs. It even works well in practice. We illustrate the potential behind it with a real-life DHCP protocol example, which we analyze by means of tool chain support.

Subproject(s): S2

Abstract (click to open/close)

This report discusses the analysis of first-order probabilistic timed automata (FPTA) by a combination of hierarchic first-order superposition-based theorem proving and probabilistic model checking. We develop the overall semantics of FPTAs and prove soundness and completeness of our method for reachability properties. Basically, we decompose FPTAs into their time plus first-order logic aspects on the one hand, and their probabilistic aspects on the other hand. Then we exploit the time plus first-order behavior by hierarchic superposition over linear arithmetic. The result of this analysis is the basis for the construction of a reachability equivalent (to the original FPTA) probabilistic timed automaton to which probabilistic model checking is finally applied. The hierarchic superposition calculus required for the analysis is sound and complete on the first-order formulas generated from FPTAs. It even works well in practice. We illustrate the potential behind it with a real-life DHCP protocol example, which we analyze by means of tool chain support.

Subproject(s): S2

Abstract (click to open/close)

We introduce Coordination Logic (CL), a new temporal logic that reasons about the interplay between behavior and informedness in distributed systems. CL provides a logical representation for the distributed realizability problem and extends the game-based temporal logics, including the alternating-time temporal logics, strategy logic, and game logic, with quantification over strategies under incomplete information. We show that the structure in CL that results from the nesting of the quantifiers is sufficient to guarantee the decidability of the logic and at the same time general enough to subsume and extend all previously known decidable cases of the distributed realizability problem.

Subproject(s): S1,S2

Abstract (click to open/close)

The authors present an automatic method for the synthesis of certificates for components in embedded real-time systems. A certificate is a small homomorphic abstraction that can transparently replace the component during model checking: if the verification with the certificate succeeds, then the component is guaranteed to be correct; if the verification with the certificate fails, then the component itself must be erroneous. The authors give a direct construction, based on a forward and backward reachability analysis of the timed system, and an iterative refinement process, which produces a series of successively smaller certificates. In their experiments, model checking the certificate is several orders of magnitude faster than model checking the original system.

Subproject(s): S1

Abstract (click to open/close)

In this article, we recall different approaches to the constraint-based, symbolic analysis of hybrid discrete-continuous systems and combine them to a technology able to address hybrid systems exhibiting both non-deterministic and probabilistic behavior akin to infinite-state Markov decision processes. To enable mechanized analysis of such systems, we extend the reasoning power of arithmetic satisfiability-modulo-theories (SMT) solving by, first, reasoning over ordinary differential equations (ODEs) and, second, a comprehensive treatment of randomized (also known as stochastic) quantification over discrete variables as well as existential quantification over both discrete and continuous variables within the mixed Boolean-arithmetic constraint system. This provides the technological basis for a constraint-based analysis of dense-time probabilistic hybrid automata, extending previous results addressing discrete-time automata (1). Generalizing SMT-based bounded model-checking of hybrid automata (2; 3), stochastic SMT including ODEs permits the direct analysis of probabilistic bounded reachability problems of dense-time probabilistic hybrid automata without resorting to approximation by intermediate finite-state abstractions.

Keywords: Probabilistic hybrid automata, bounded model checking, arithmetic constraint solving, stochastic satisfiability
Subproject(s): H1/2,H4

Abstract (click to open/close)

Stochastic satisfiability modulo theories (SSMT), which is an extension of satisfiability modulo theories with randomized quantification, has successfully been used as a symbolic technique for computing reachability probabilities in probabilistic hybrid systems. Motivated by the fact that several industrial applications call for quantitative measures that go beyond mere reachability probabilities, this paper extends SSMT to compute expected values of probabilistic hybrid systems like, e.g., mean-times to failure. Practical applicability of the proposed approach is demonstrated by a case study from networked automation systems.

Subproject(s): H1/2,H4

Abstract (click to open/close)

The FlexRay standard, developed by a cooperation of leading companies in the automotive industry, is a robust communication protocol for distributed components in modern vehicles. In this paper, we present the first timed automata model of its physical layer protocol, and we use automatic verification to prove fault tolerance under several error models and hardware assumptions. The key challenge in the analysis is that the correctness of the protocol relies on the interplay of the bit-clock alignment mechanism with the precise timing behavior of the underlying asynchronous hardware. We give a general hardware model that is parameterized in low-level timing details such as hold times and propagation delays. Instantiating this model for a realistic design from the Nangate Open Cell Library, and verifying the resulting model using the real-time model checker Uppaal, we show that the communication system meets, and in fact exceeds, the fault-tolerance guarantees claimed in the FlexRay specification.

Subproject(s): S1

Subproject(s): S1

Abstract (click to open/close)

Given a parametric Markov model, we consider the problem of computing the rational function expressing the probability of reaching a given set of states. To attack this principal problem, Daws has suggested to first convert the Markov chain into a finite automaton, from which a regular expression is computed. Afterwards, this expression is evaluated to a closed form function representing the reachability probability. This paper investigates how this idea can be turned into an effective procedure. It turns out that the bottleneck lies in the growth of the regular expression relative to the number of states (n (log n) ). We therefore proceed differently, by tightly intertwining the regular expression computation with its evaluation. This allows us to arrive at an effective method that avoids this blow up in most practical cases. We give a detailed account of the approach, also extending to parametric models with rewards and with non-determinism. Experimental evidence is provided, illustrating that our implementation provides meaningful insights on non-trivial models.

Subproject(s): S2,S3

Abstract (click to open/close)

We present PARAM 1.0, a model checker for parametric discrete-time Markov chains (PMCs). PARAM can evaluate temporal properties of PMCs and certain extensions of this class. Due to parametricity, evaluation results are polynomials or rational functions. By instantiating the parameters in the result function, one can cheaply obtain results for multiple individual instantiations, based on only a single more expensive analysis. In addition, it is possible to post-process the result function symbolically using for instance computer algebra packages, to derive optimum parameters or to identify worst cases.

Subproject(s): S2, S3

Abstract (click to open/close)

We present PASS a tool that analyzes concurrent probabilistic programs, which map to potentially infinite Markov decision processes. PASS is based on predicate abstraction and abstraction refinement and scales to programs far beyond the reach of numerical methods which operate on the full state space of the model. The computational engines we use are SMT solvers to compute finite abstractions, numerical methods to compute probabilities and interpolation as part of abstraction refinement. PASS has been successfully applied to network protocols and serves as a test platform for different refinement methods.

Subproject(s): S2,S3

Abstract (click to open/close)

In this paper, we explore the potential of the theory of nested words for partial correctness proofs of recursive programs. Our conceptual contribution is a simple framework that allows us to shine a new light on classical concepts such as Floyd/Hoare proofs and predicate abstraction in the context of recursive programs. Our technical contribution is an interpolant-based software model checking method for recursive programs. The method avoids the costly construction of the abstract transformer by constructing a nested word automaton from an inductive sequence of `nested interpolants' (i.e., interpolants for a nested word which represents an infeasible error trace).

Subproject(s): R1

Abstract (click to open/close)

We describe the gap heuristic for the pancake problem, which dramatically outperforms current abstraction-based heuristics for this problem. The gap heuristic belongs to a family of landmark heuristics that have recently been very successfully applied to planning problems.

Subproject(s): S1

Abstract (click to open/close)

We introduce the Scanalyzer planning domain, a domain for classical planning which models the problem of automatic greenhouse logistic management. At its mathematical core, the Scanalyzer domain is a permutation problem with striking similarities to common search benchmarks such as Rubik's Cube or TopSpin. At the same time, it is also a real application domain, and efficient algorithms for the problem are of considerable practical interest. The Scanalyzer domain was used as a benchmark for sequential planners at the last International Planning Competition. The competition results show that domain-independent automated planners can find solutions of comparable quality to those generated by specialized algorithms developed by domain experts, while being considerably more flexible.

Subproject(s): S1

Abstract (click to open/close)

The pancake problem is a famous search problem where the objective is to sort a sequence of objects (pancakes) through a minimal number of prefix reversals flips. The best approaches for the problem are based on heuristic search with abstraction (pattern database) heuristics. We present a new class of abstractions for the pancake problem called relative-order abstractions. Relative-order abstractions have three advantages over the object-location abstractions considered in previous work. First, they are size-independent, ie , do not need to be tailored to a particular instance size of the pancake problem. Second, they are more compact in that they can represent a larger number of pancakes within abstractions of bounded size. Finally, they can exploit symmetries in the problem specification to allow multiple heuristic lookups, significantly improving search performance over a single lookup. Our experiments show that compared to object-location abstractions, our new techniques lead to an improvement of one order of magnitude in runtime and up to three orders of magnitude in the number of generated states.

Subproject(s): S1

Abstract (click to open/close)

We present a numerical approximation technique for the analysis of continuous-time Markov chains that describe networks of biochemical reactions and play an important role in the stochastic modeling of biological systems.Our approach is based on the construction of a stochastic hybrid model in which certain discrete random variables of the original Markov chain are approximated by continuous deterministic variables. We compute the solution of the stochastic hybrid model using a numerical algorithm that discretizes time and in each step performs a mutual update of the transient probability distribution of the discrete stochastic variables and the values of the continuous deterministic variables. We implemented the algorithm and we demonstrate its usefulness and efficiency on several case studies from systems biology.

Subproject(s): S3,H4

Abstract (click to open/close)

Due to the increasing use of more and more complex computerized systems in safety-critical applications, formal verification of such systems is of growing importance. Among the most successful methods in formal verification of finite-state systems is bounded model checking (BMC), a technique for checking whether an unsafe system state is reachable within a fixed number of steps. BMC belongs to a class of verification algorithms having in common that the verification task is reduced to the problem of checking the satisfiability of a propositional formula or a series thereof. Though originally formulated for discrete transition systems only, BMC is in principle also applicable to hybrid discrete-continuous systems, which naturally arise e.g. in the field of embedded systems where digital (discrete) controllers are coupled with analog (continuous) physical plants. The BMC formulae arising from such systems are, however, no longer purely propositional, but usually comprise complex Boolean combinations of arithmetic constraints over real-valued variables, thus entailing the need for new decision procedures to solve them. This thesis deals with the development of such procedures. A key component of the algorithms we present is the DPLL procedure for solving Boolean formulae which are in conjunctive normal form (CNF). As a first contribution, we demonstrate that the acceleration techniques, which enabled the enormous performance gains of Boolean SAT solvers in the recent past, generalize smoothly to DPLL-based procedures for solving systems of pseudo-Boolean constraints, a much more concise representation of Boolean functions than CNFs. Second, we investigate how to efficiently couple a linear programming routine with a DPLL-based SAT solver in order to obtain a solver which is tailored for BMC of hybrid systems with linear dynamics. In particular, we examine how to exploit the unique characteristics of BMC formulae and the incremental nature of BMC for various optimizations inside the solver. Finally, we present our main contribution, a tight integration of the DPLL procedure with interval constraint solving, resulting in an algorithm, called iSAT, which generalizes the DPLL procedure and is capable of solving arbitrary Boolean combinations of nonlinear arithmetic constraints over the reals, even such involving transcendental functions. We demonstrate the applicability of our methods using benchmarks from the envisaged application domain.

Subproject(s): H1/2

Abstract (click to open/close)

Already in Lamport's bakery algorithm, integers are used for fair schedulers of concurrent processes. In this paper, we present the extension of a fair scheduler from `static control' (the number of processes is fixed) to `dynamic control' (the number of processes changes during execution). We believe that our results shed new light on the concept of fairness in the setting of dynamic control.

Subproject(s): S2

Abstract (click to open/close)

We are concerned with the availability of systems, defined as the ratio between time of correct functioning and uptime. We propose to model guaranteed availability in terms of regular availability expressions (rae) and emph availability automata. We prove that the intersection problem of rae is undecidable. We establish a Kleene theorem that shows the equivalence of the formalisms and states precise correspondence of flat rae and simple availability automata. For these automata, we provide an extension of the powerset construction for finite automata due to Rabin and Scott. As a consequence, we can state a complementation algorithm. This enables us to solve the synthesis problem and to reduce model checking of availability properties to reachability.

Subproject(s): R1

Abstract (click to open/close)

Disunification is an extension of unification to first-order formulae over syntactic equality atoms. Instead of considering only syntactic equality, I extend a disunification algorithm by Comon and Delor to ultimately periodic interpretations, i.e. minimal many-sorted Herbrand models of predicative Horn clauses and, for some sorts, equations of the form sl(x){sk(x). The extended algorithm is terminating and correct for ultimately periodic interpretations over a finite signature and gives rise to a decision procedure for the satisfiability of equational formulae in ultimately periodic interpretations. As an application, I show how to apply disunification to compute the completion of predicates with respect to an ultimately periodic interpretation. Such completions are a key ingredient to several inductionless induction methods.

Subproject(s): H1/2

Abstract (click to open/close)

Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a minimal term-generated model for the theory. Proving universal properties with respect to a saturated theory directly leads to a modification of the minimal model's term-generated domain, as new Skolem functions are introduced. For many applications, this is not desired. Therefore, we propose the first superposition calculus that can explicitly represent existentially quantified variables and can thus compute with respect to a given domain. This calculus is sound and refutationally complete in the limit for a first-order fixed domain semantics. For saturated Horn theories and classes of positive formulas, we can even employ the calculus to prove properties of the minimal model itself, going beyond the scope of known superposition-based approaches.

Subproject(s): H1/2

Abstract (click to open/close)

Verification problems are often expressed in a language which mixes several theories. A natural question to ask is whether one can use decision procedures for individual theories to construct a decision procedure for the union theory. In the cases where this is possible one has a powerful method at hand to handle complex theories effectively. The setup considered in this thesis is that of one base theory which is extended by one or more theories. The question is if and when a given ground satisfiability problem in the extended setting can be effectively reduced to an equi-satisfiable problem over the base theory. A case where this reductive approach is always possible is that of so-called local theory extensions. The theory of local extensions is developed and some applications concerning monotone functions are given. Then the theory of local theory extensions is generalized in order to deal with data structures that exhibit local behavior. It will be shown that a suitable fragment of both the theory of arrays and the theory of pointers is local in this broader sense. Finally, the case of more than one theory extension is discussed. In particular, a modularity result is given that under certain circumstances the locality of each of the extensions lifts to locality of the entire extension. The reductive approach outlined above has become particularly relevant in recent years due to the rise of powerful solvers for background theories common in verification tasks. These so-called SMT-solvers effectively handle theories such as real linear or integer arithmetic. As part of this thesis, a program called H-PILoT was implemented which carries out reductive reasoning for local theory extensions. H-PILoT found applications in mathematics, multiple-valued logics, data-structures and reasoning in complex systems

Subproject(s): R1,H3

Abstract (click to open/close)

In this paper we study theory combinations over non-disjoint signatures in which hierarchical and modular reasoning is possible. We use a notion of locality of a theory extension parameterized by a closure operator on ground terms. We give criteria for recognizing these types of theory extensions. We then show that combinations of extensions of theories which are local in this extended sense have also a locality property and hence allow modular and hierarchical reasoning. We thus obtain parameterized decidability and complexity results for many (combinations of) theories important in verification.

Subproject(s): R1

Abstract (click to open/close)

In this paper we study theory combinations over non-disjoint signatures in which hierarchical and modular reasoning is possible. We use a notion of locality of a theory extension parameterized by a closure operator on ground terms. We give criteria for recognizing these types of theory extensions. We then show that combinations of extensions of theories which are local in this extended sense also have a locality property and hence allow modular and hierarchical reasoning. We thus obtain parameterized decidability and complexity results for many (combinations of) theories important in verification.

Subproject(s): R1

Abstract (click to open/close)

This system description provides an overview of H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions), a program for hierarchical reasoning in extensions of logical theories. H-PILoT reduces deduction problems in the theory extension to deduction problems in the base theory. Specialized provers and standard SMT solvers can be used for testing the satisfiability of the formulae obtained after the reduction. For a certain type of theory extension (namely for local theory extensions) this hierarchical reduction is sound and complete and -- if the formulae obtained this way belong to a fragment decidable in the base theory -- H-PILoT provides a decision procedure for testing satisfiability of ground formulae, and can also be used for model generation.

Subproject(s): R1,H3

Abstract (click to open/close)

Information-handling systems are becoming ever more complex. They may be pure hardware or software systems, or complex systems of hardware and software that act in a real-world environment. Verification is a method to ensure that systems behave in the expected way, which is a necessity for safety-critical applications like automatic railway control. The size of such systems makes manual verification impossible. Therefore, we need automatic or computer-aided verification procedures. Automated reasoning is already widely used in the analysis and verification of systems. For a restricted class of systems, the resulting verification problems are inherently finite and can be solved efficiently. For complex systems, such finiteness cannot be expected. To express and prove properties of these systems, we need a formal language and reasoners that can deal with universal quantification, arithmetic expressions and unbounded data structures at the same time. Thus, in recent years there has been new interest in the handling of first-order formulas modulo a given background theory. The problem is known to be undecidable in general, and research focuses mostly on methods that solve many problem instances quickly, but sacrifice completeness. We take a different approach and focus on instances of this problem that we can show to be decidable. In this way we can solve the resulting problems efficiently and guarantee termination. This work is based on research by Sofronie-Stokkermans on local theory extensions and on work by Ganzinger and Korovin on instantiation-based first-order theorem proving. We extend the existing work on local theory extensions, giving new examples of axioms which satisfy a locality condition and using ideas from instantiation-based first-order theorem proving to make local reasoning more efficient. Furthermore, we show that local theory extensions allow us to decide certain verification problems for parameterized systems and develop increasingly complex system models of an automatic train controller on which we demonstrate how to use local reasoning to verify safety properties of such systems.

Subproject(s): R1,H3

Abstract (click to open/close)

In this paper we present two different parallelization schemes for the SMT solver iSAT, based on (1) the distribution of work by dividing the search space into disjoint parts and exploring them in parallel, thereby exchanging learnt information, and (2) a portfolio approach, where the entire benchmark instance is explored in parallel by several copies of the same solver but using different heuristics to guide the search. We also combine both approaches such that solvers examine disjoint parts of the search space using different heuristics. The main contribution of the paper is to study the performances of different techniques for parallelizing iSAT.

Subproject(s): H1/2

Abstract (click to open/close)

The Markov Reward Model Checker (MRMC) is a software tool for verifying properties over probabilistic models. It supports PCTL and CSL model checking, and their reward extensions. Distinguishing features of MRMC are its support for computing time- and reward-bounded reachability probabilities, (property-driven) bisimulation minimization, and precise on-the-fly steady-state detection. Recent tool features include time-bounded reachability analysis for continuous-time Markov decision processes (CTMDPs) and CSL model checking by discrete-event simulation. This paper presents the tool’s current status and its implementation details.

Keywords: Model checking,Markov chains,CTMC,DTMC,MRM,CTMDP, Numerical analysis,Discrete-event simulation,Bisimulation minimization
Subproject(s): S3

Abstract (click to open/close)

Landmarks for a planning problem are subgoals that are necessarily made true at some point in the execution of any plan. Since verifying that a fact is a landmark is PSPACE-complete, earlier approaches have focused on finding landmarks for the delete relaxation Pi ^+. Furthermore, some of these approaches have approximated this set of landmarks, although it has been shown that the complete set of causal delete-relaxation landmarks can be identified in polynomial time by a simple procedure over the relaxed planning graph. Here, we give a declarative characterisation of this set of landmarks and show that the procedure computes the landmarks described by our characterisation. Building on this, we observe that the procedure can be applied to any delete-relaxation problem and take advantage of a recent compilation of the m-relaxation of a problem into a problem with no delete effects to extract landmarks that take into account delete effects in the original problem. We demonstrate that this approach finds strictly more causal landmarks than previous approaches and discuss the relationship between increased computational effort and experimental performance, using these landmarks in a recently proposed admissible landmark-counting heuristic.

Subproject(s): S1

Abstract (click to open/close)

Traditional incremental SAT solvers have achieved great success in the domain of Bounded Model Checking (BMC). However, modern solvers depend on advanced preprocessing procedures to obtain high levels of performance. Unfortunately, many preprocessing techniques such as a variable and (blocked) clause elimination cannot be directly used in an incremental manner. This work focuses on extending these techniques and Craig interpolation so that they can be used effectively together in incremental SAT solving (in the context of BMC). The techniques introduced here doubled the performance of our BMC solver on both SAT and UNSAT problems. For UNSAT problems, preprocessing had the added advantage that Craig interpolation was able to find the fixed point sooner, reducing the number of incremental SAT iterations. Furthermore, our ideas seem to perform better as the benchmarks become larger, and/or deeper, which is exactly when they are needed. Lastly, our methods can be extended to other SAT based BMC tools to achieve similar speedups.

Keywords: BMC, Craig Interpolation, model checking, Preprocessing, SAT
Subproject(s): H1/2

Abstract (click to open/close)

When planning in an uncertain environment, one is often interested in finding a contingent plan that prescribes appropriate actions for all possible states that may be encountered during the execution of the plan. We consider the problem of finding strong cyclic plans for fully observable nondeterministic (FOND) planning problems. The algorithm we choose is LAO*, an informed explicit state search algorithm. We investigate the use of pattern database (PDB) heuristics to guide LAO* towards goal states. To obtain a fully domainindependent planning system, we use an automatic pattern selection procedure that performs local search in the space of pattern collections. The evaluation of our system on the FOND benchmarks of the Uncertainty Part of the International Planning Competition 2008 shows that our approach is competitive with symbolic regression search in terms of problem coverage, speed, and plan quality.

Subproject(s): S1

Abstract (click to open/close)

Verification of real-time systems -- e.g. communication protocols or embedded controllers -- is an important task. One method to detect errors is called bounded model checking (BMC). In BMC the system is iteratively unfolded and then transformed into a satisfiability problem. If an appropriate solver finds the k-th instance to be satisfiable a counterexample for a given safety property has been found. In this paper we present a first approach to apply BMC to networks of timed automata (that is a system of several interacting subautomata) where parts of the network are unspecified (so called blackboxes). Here, we would like to answer the question of unrealizability, that is, is there a path of a certain length violating a safety property regardless of the implementation of the blackboxes. We provide solutions to this problem for two timed automata communication models. For the simple synchronization model, a BMC approach based on fixed transitions is introduced resulting in a SAT-Modulo-Theory formula. With respect to the use of bounded integer variables for communication, we prove unrealizability by introducing universal quantification, yielding more advanced quantified SAT-Modulo-Theory formulas.

Subproject(s): S1

Abstract (click to open/close)

This paper focuses on bounded invariant checking for partially specified circuits -- designs containing so-called blackboxes -- using the well known 01X- and QBF-encoding techniques. For detecting counterexamples, modeling the behavior of a blackbox using 01X-encoding is rather coarse as it limits what problems can be verified. We introduce the idea of 01X-hardness, mainly the classification of problems for which this encoding technique does not provide any useful information about the existence of a counterexample. Furthermore, we provide a proof for 01X-hardness based on Craig interpolation, and show how the information contained within the proof can be used to determine heuristically which blackbox outputs to model in a more precise way. This allows us to formulate the problem using an optimized hybrid 01X/QBF-encoding, resulting in problems that are much easier to solve than the pure QBF approach. Finally, multiple state-of-the-art QBF-solvers are shown to perform well on a range of blackbox circuit problems using the proposed method.

Subproject(s): S1,H1/2

Abstract (click to open/close)

This paper focuses on bounded invariant checking for partially specified circuits -- designs containing so-called blackboxes -- using the well known 01X- and QBF-encoding techniques. For detecting counterexamples, modeling the behavior of a blackbox using 01X-encoding is fast, but rather coarse as it limits what problems can be verified. We introduce the idea of 01X-hardness, mainly the classification of problems for which this encoding technique does not provide any useful information about the existence of a counterexample. Furthermore, we provide a proof for 01X-hardness based on Craig interpolation, and show how the information contained within the Craig interpolant or unsat-core can be used to determine heuristically which blackbox outputs to model in a more precise way. We then compare 01X, QBF and multiple hybrid modeling methods. Finally, our total workflow along with multiple state-of-the-art QBF-solvers are shown to perform well on a range of industrial blackbox circuit problems.

Subproject(s): S1,H1/2

Abstract (click to open/close)

We introduce a novel method that integrates BDD-based symbolic model checking into SAT-based bounded model checking in the presence of unknowns. By incorporating both distinctively different methods, our new hybrid verification tool can take advantage of what each type of model checking has to offer. We present a case study for which both the BDD-based method as well as the SAT-based method are unable to provide a proof that the considered property fails, but that can be solved using the integrated approach.

Subproject(s): S1

Abstract (click to open/close)

We investigate layered composition for real-time systems modelled as (networks of) timed automata (TA). Our contributions are the following: (1) We first formulate the principles of layering and transition independence for TA, and demonstrate the validity of the communication closed layer (CCL) laws in such a setting, by means of an operator for layered composition that is intermediate between parallel and sequential composition. (2) Next, we introduce the principles of input/output (i/o) and partial-order equivalences, and show that such equivalences are preserved when the layered composition operator is replaced by sequential composition within the expressions appearing in the CCL laws. (3) We finally proceed to show that such layering (together with equivalences obtained through the CCL laws) can be useful in the design and verification of dense real-time systems that consist of a network of interacting components, by bringing about a reduction of the state-space through the exploitation of transition independence. Such a reduction by means of layering and the resulting equivalences are shown to complement the well-studied partial order reduction approach to the model-checking of networks of TA. This is illustrated by considering a collision avoidance protocol that was developed for an audio/video system of Bang and Olufsen.

Subproject(s): R1

Abstract (click to open/close)

In this paper we present a solver for Quantified Boolean Formulas (QBFs) which is based on And-Inverter Graphs (AIGs). We use a new quantifier elimination method for AIGs, which heuristically combines cofactor-based quantifier elimination with quantification using BDDs and thus benefits from the strengths of both data structures. Moreover, we present a novel SAT-based method for preprocessing QBFs that is able to efficiently detect variables with forced truth assignments, allowing for an elimination of these variables from the input formula. We describe the used algorithm which heavily relies on the incremental features of modern SAT solvers. Experimental results demonstrate that our preprocessing method can significantly improve the performance of QBF preprocessing and thus is able to accelerate the overall solving process when used in combination with state-of-the-art QBF-solvers. In particular, we integrated the preprocessing technique as well as the quantifier elimination method into the QBF-solver AIGSolve, allowing it to outperform state-of-the-art solvers.

Subproject(s): H3

Abstract (click to open/close)

Hybrid systems are models for complex physical systems and have become a widely used concept for understanding their behaviour. Many applications are safety-critical, including car, railway, and air traffic control, robotics, physical-chemical process control, and biomedical devices. Hybrid systems analysis studies how we can build computerised controllers for physical systems which are guaranteed to meet their design goals. This is the first book that leverages the power of logic for hybrid systems. The author develops a coherent logical approach for systematic hybrid systems analysis, covering its theory, practice, and applications. It is further shown how the developed verification techniques can be used to study air traffic and railway control systems. This book is intended for researchers, postgraduates, and professionals who are interested in hybrid systems analysis, cyberphysical or embedded systems design, logic and theorem proving, or transportation and automation.

Subproject(s): H3

Abstract (click to open/close)

The automated inference of quantified invariants is considered one of the next challenges in software verification. The question of the right precision-efficiency tradeoff for the corresponding program analyses here boils down to the question of the right treatment of disjunction below and above the universal quantifier. In the closely related setting of shape analysis one uses the focus operator in order to adapt the treatment of disjunction (and thus the efficiency-precision tradeoff) to the individual program statement. One promising research direction is to design parameterized versions of the focus operator which allow the user to fine-tune the focus operator not only to the individual program statements but also to the specific verification task. We carry this research direction one step further. We fine-tune the focus operator to each individual step of the analysis (for a specific verification task). This fine-tuning must be done automatically. Our idea is to use counterexamples for this purpose. We realize this idea in a tool that automatically infers quantified invariants for the verification of a variety of heap-manipulating programs.

Subproject(s): S2

Abstract (click to open/close)

Safety verification of hybrid systems is undecidable, except for very special cases. In this paper, we circumvent undecidability by providing an algorithm that can verify safety and provably terminates for all robust and safe problem instances. It need not necessarily terminate for problem instances that are unsafe or non-robust. A problem instance x is robust iff the given property holds not only for x itself, but also when x is perturbed a little bit. Since, in practice, well-designed hybrid systems are usually robust, this implies that the algorithm terminates for the cases occurring in practice. In contrast to earlier work, our result holds for a very general class of hybrid systems, and it uses a continuous time model.

Subproject(s): H1/2

Abstract (click to open/close)

In this paper, we present a method for computing a basin of attraction to a target region for polynomial ordinary differential equations. This basin of attraction is ensured by a Lyapunov-like polynomial function that we compute using an interval based branch-and-relax algorithm. This algorithm relaxes the necessary conditions on the coefficients of the Lyapunov-like function to a system of linear interval inequalities that can then be solved exactly. It iteratively refines these relaxations in order to ensure that, whenever a nondegenerate solution exists, it will eventually be found by the algorithm. Application of an implementation to a range of benchmark problems shows the usefulness of the approach.

Subproject(s): H4

Abstract (click to open/close)

We empirically examine several ways of exploiting the information of multiple heuristics in a satisficing best-first search algorithm, comparing their performance in terms of coverage, plan quality, speed, and search guidance. Our results indicate that using multiple heuristics for satisficing search is indeed useful. Among the combination methods we consider, the best results are obtained by the alternation method of the ``Fast Diagonally Downward'' planner.

Subproject(s): S1

Abstract (click to open/close)

Interpolation is an important component of recent methods for program verification. It provides a natural and effective means for computing the separation between the sets of good and bad states. The existing algorithms for interpolant generation are proof-based: They require explicit construction of proofs, from which interpolants can be computed. Construction of such proofs is a difficult task. We propose an algorithm for the generation of interpolants for the combined theory of linear arithmetic and uninterpreted function symbols that does not require a priori constructed proofs to derive interpolants. It uses a reduction of the problem to constraint solving in linear arithmetic, which allows application of existing highly optimized Linear Programming solvers in a black-box fashion. We provide experimental evidence of the practical applicability of our algorithm.

Subproject(s): R1

Abstract (click to open/close)

Embedded systems are widely used for supporting our every day life. In the area of safety-critical systems human life often depends on the system's correct behavior. Many of such systems are hard real-time systems, so that the notion of correctness not only means functional correctness. They additionally have to obey stringent timing constraints, i.e. timely task completion under all circumstances is essential. An example for such a safety-critical system is the flight control computer in an airplane, which is responsible for stability, attitude and path control. In order to derive guarantees on the timing behavior of hard real-time systems, the worst-case execution time (WCET) of each task in the system has to be determined. Saarland University and AbsInt GmbH have successfully developed the aiT WCET analyzer for computing safe upper bounds on the WCET of a task. The computation is mainly based on abstract interpretation of timing models of the processor and its periphery. Such timing models are currently hand-crafted by human experts. Therefore their implementation is a time-consuming and Modern processors or system controllers are automatically synthesized out of formal hardware specifications like VHDL or Verilog. Besides the system' functional behavior, such specifications provide all information needed for the creation of a timing model. But due to their size and complexity, manually examining the sources is even more complex than only looking at the processor manuals. Moreover, this would not reduce the effort nor the probability of implementation errors. To face this problem, this paper proposes a method for semi-automatically deriving suitable timing models out of formal hardware specifications in VHDL that fit to the tool chain of the aiT WCET analyzer. By this, we reduce the creation time of timing models from months to weeks.

Subproject(s): R2

Abstract (click to open/close)

We study possibilities of reasoning about extensions of base theories with functions which satisfy certain recursion and homomorphism properties. Our focus is on emphasizing possibilities of hierarchical and modular reasoning in such extensions and combinations thereof. 1) We show that the theory of absolutely free constructors is local, and locality is preserved also in the presence of selectors. These results are consistent with existing decision procedures for this theory (e.g. by Oppen). 2) We show that, under certain assumptions, extensions of the theory of absolutely free constructors with functions satisfying a certain type of recursion axioms satisfy locality properties, and show that for functions with values in an ordered domain we can combine recursive definitions with boundedness axioms without sacrificing locality. We also address the problem of only considering models whose data part is the em initial term algebra of such theories.3) We analyze conditions which ensure that similar results can be obtained if we relax some assumptions about the absolute freeness of the underlying theory of data types, and illustrate the ideas on an example from cryptography. The locality results we establish allow us to reduce the task of reasoning about the class of recursive functions we consider to reasoning in the underlying theory of data structures (possibly combined with the theories associated with the co-domains of the recursive functions). As a by-product, the methods we use provide a possibility of presenting in a different light (and in a different form) locality phenomena studied in cryptography; we believe that they will allow to better separate rewriting from proving, and thus to give simpler proofs.

Subproject(s): R1

Abstract (click to open/close)

We study certain classes of verification problems for parametric reactive and hybrid systems, and identify the types of logical theories which can be used for modeling such systems and the reasoning tasks which need to be solved in this context. We identify properties of the underlying theories which ensure that these classes of verification problems can be solved efficiently, give examples of theories with the desired properties, and illustrate the methods we use on several examples.

Subproject(s): R1,H3

Abstract (click to open/close)

The stochastic Boolean satisfiability (SSAT) problem was introduced by Papadimitriou in 1985 by adding a probabilistic model of uncertainty to propositional satisfiability through randomized quantification. SSAT has many applications, e.g., in probabilistic planning and, more recently by integrating arithmetic, in probabilistic model checking. In this paper, we first present a new result on the computational complexity of SSAT: SSAT remains PSPACE-complete even for its restriction to 2CNF. Second, we propose a sound and complete resolution calculus for SSAT complementing the classical backtracking search algorithms.

Subproject(s): H1/2,H4

Abstract (click to open/close)

This paper addresses the problem of assigning tasks to embedded control units. The units are considered to be connected via a bus, and tasks may already be deployed onto the units. To save costs, the objective is to insert as many new tasks onto the system as possible. In this setting, to support early design decisions, we present an approximative and fast pre-analysis of the system. We introduce spare-time analysis and the analysis of maximal allowed worst-case execution time to simplify the problem and to achieve a fast solving algorithm, which we implement as mixed-integer linear problem. We conduct experiments to investigate the scalability of the approach with the result that for input sizes of up to 160 tasks with up to 50% not-yet-deployed tasks a solution is found in many cases within reasonable time, our machine needs in the average case 150s. With a reference example, taken from literature, we compare our approach with a similar method and show that our approach is faster.

Subproject(s): R2

Abstract (click to open/close)

We present "spotlight abstraction" as a generic abstraction technique for the analysis of systems comprising an unbounded number of communicating agents. The abstraction principle is heterogeneous in the sense that the behaviour of a finite number of agents is preserved while the others are only abstractly represented. The precision of the abstraction can be tuned by an iterative procedure based on the analysis of counterexamples. Going beyond existing work, we show how to use the spotlight principle for analysing systems where the physical position of agents is relevant. To this end, we put the spotlight on areas rather than on fixed sets of agents.

Keywords: Spotlight Abstraction, Verification, Dynamic Communication Systems
Subproject(s): S2

Abstract (click to open/close)

This paper investigates relative precision and optimality of analyses for concurrent probabilistic systems. Aiming at the problem at the heart of probabilistic model checking – computing the probability of reaching a particular set of states – we leverage the theory of abstract interpretation. With a focus on predicate abstraction, we develop the first abstract-interpretation framework for Markov decision processes which admits to compute both lower and upper bounds on reachability probabilities. Further, we describe how to compute and approximate such abstractions using abstraction refinement and give experimental results.

Subproject(s): S2,S3

Abstract (click to open/close)

Directed model checking is a well-established technique to efficiently tackle the state explosion problem when the aim is to find error states in concurrent systems. Although directed model checking has proved to be very successful in the past, additional search techniques provide much potential to efficiently handle larger and larger systems. In this work, we propose a novel technique for traversing the state space based on interference contexts. The basic idea is to preferably explore transitions that interfere with previously applied transitions, whereas other transitions are deferred accordingly. Our approach is orthogonal to the model checking process and can be applied to a wide range of search methods. We have implemented our method and empirically evaluated its potential on a range of non-trivial case studies. Compared to standard model checking techniques, we are able to detect subtle bugs with shorter error traces, consuming less memory and time.

Subproject(s): R3

Abstract (click to open/close)

Bisimulation reduction is a classical means to fight the infamous state space explosion problem, which limits the applicability of automated methods for verification like model checking. A signature-based method, originally developed by Blom and Orzan for labeled transition systems and adapted for Markov chains by Derisavi, has proved to be very efficient. It is possible to implement it symbolically using binary decision diagrams such that it is able to handle very large state spaces efficiently. We will show, however, that for Markov chains this algorithm suffers from numerical instabilities, which often result in too large quotient systems. We will present and experimentally evaluate two different approaches to avoid these problems: first the usage of rational arithmetic, and second an approach not only to represent the system structure but also the transition rates symbolically. In addition, this allows us to modify their actual values after the quotient computation.

Subproject(s): S3

Abstract (click to open/close)

Model checkers for concurrent probabilistic systems have become very popular within the last decade. The study of long-run average behavior has however received only scant attention in this area, at least from the implementation perspective. This paper studies the problem of how to efficiently realize an algorithm for computing optimal long-run average reward values for concurrent probabilistic systems. At its core is a variation of Howard and Veinott's algorithm for Markov decision processes, where symbolic and non-symbolic representations are intertwined in an effective manner: the state space is represented using binary decision diagrams, while the linear equation systems which have to be solved for the induced Markov chains to improve the current scheduler are solved using an explicit state representation. In order to keep the latter small, we apply a symbolic bisimulation minimization algorithm to the induced Markov chain. The scheduler improvement step itself is again performed on symbolic data structures. Practical evidence shows that the implementation is effective, and sometimes uses considerably less memory than a fully explicit implementation.

Subproject(s): S3

Abstract (click to open/close)

State space lumping is one of the classical means to fight the state space explosion problem in state-based performance evaluation and verification. Particularly when numerical algorithms are applied to analyze a Markov model, one often observes that those algorithms do not scale beyond systems of moderate size. To alleviate this problem, symbolic lumping algorithms have been devised to effectively reduce very large--but symbolically represented--Markov models to moderate size explicit representations. This lumping step partitions the Markov model in such a way that any numerical analysis carried out on the lumped model is guaranteed to produce exact results for the original system. But even this lumping preprocessing may fail due to time or memory limitations. This paper discusses the two main approaches to symbolic lumping, and combines them to improve on their respective limitations. The algorithm automatically converts between known symbolic partition representations in order to provide a trade-off between memory consumption and runtime. We show how to apply this algorithm for the lumping of Markov chains, but the same techniques can be adapted in a straightforward way to other models like Markov reward models, labeled transition systems, or interactive Markov chains.

Subproject(s): S3

Abstract (click to open/close)

Hermanns has introduced interactive Markov chains (IMCs) which arise as an orthogonal extension of labelled transition systems and continuous-time Markov chains (CTMCs). IMCs enjoy nice compositional aggregation properties which help to minimize the state space incrementally. However, the model checking problem for IMCs remains unsolved apart from those instances, where the IMC can be converted into a CTMC. This paper tackles this problem: We interpret the continuous stochastic logic (CSL) over IMCs and define the semantics of probabilistic CSL formulas with respect to the class of fully time and history dependent schedulers. Our main contribution is an efficient model checking algorithm for verifying CSL formulas on IMCs. Moreover, we show the applicability of our approach and provide some experimental results.

Subproject(s): S3

Abstract (click to open/close)

The interplay of random phenomena and continuous real-time control deserves increased attention for instance in wireless sensing and control applications. Safety verification for such systems thus needs to consider probabilistic variations of systems with hybrid dynamics. In safety verification of classical hybrid systems we are interested in whether a certain set of unsafe system states can be reached from a set of initial states. In the probabilistic setting, we may ask instead whether the probability of reaching unsafe states is below some given threshold. In this paper, we consider probabilistic hybrid systems and develop a general abstraction technique for verifying probabilistic safety problems. This gives rise to the first mechanisable technique that can, in practice, formally verify safety properties of non-trivial continuous-time stochastic hybrid systems—without resorting to point-wise discretisation. Moreover, being based on arbitrary abstractions computed by tools for the analysis of non-probabilistic hybrid systems, improvements in effectivity of such tools directly carry over to improvements in effectivity of the technique we describe. We demonstrate the applicability of our approach on a number of case studies, tackled using a prototypical implementation.

Subproject(s): H4

Abstract (click to open/close)

Bounded model checking (BMC) is an incremental refutation technique to search for counterexamples of increasing length. The existence of a counterexample of a fixed length is expressed by a first-order logic formula that is checked for satisfiability using a suitable solver. We apply communicating parallel solvers to check satisfiability of the BMC formulae. In contrast to other parallel solving techniques, our method does not parallelize the satisfiability check of a single formula, but the parallel solvers work on formulae for different counterexample lengths. We adapt the method of constraint sharing and replication of Shtrichman, originally developed for sequential BMC, to the parallel setting. Since the learning mechanism is now parallelized, it is not obvious whether there is a benefit from the concepts of Shtrichman in the parallel setting. We demonstrate on a number of benchmarks that adequate communication between the parallel solvers yields the desired results.

Keywords: parallel programs, bounded model checking, SAT solving, linear programming, hybrid systems
Subproject(s): H1/2

Abstract (click to open/close)

The hierarchical superposition based theorem proving calculus of Bachmair, Ganzinger, and Waldmann enables the hierarchic combination of a theory with full first-order logic. If a clause set of the combination enjoys a sufficient completeness criterion, the calculus is even complete. We instantiate the calculus for the theory of linear arithmetic. In particular, we develop new effective versions for the standard superposition redundancy criteria taking the linear arithmetic theory into account. The resulting calculus is implemented in SPASS(LA) and extends the state of the art in proving properties of first-order formulas over linear arithmetic.

Subproject(s): S2

Abstract (click to open/close)

The hierarchical superposition based theorem proving calculus of Bachmair, Ganzinger, and Waldmann enables the hierarchic combination of a theory with full first-order logic. If a clause set of the combination enjoys a sufficient completeness criterion, the calculus is even complete. We instantiate and refine the calculus for the theory of linear arithmetic. In particular, we develop new effective versions for the standard superposition redundancy criteria taking the linear arithmetic theory into account. The resulting calculus is implemented in SPASS(LA) and extends the state of the art in proving properties of first-order formulas over linear arithmetic.

Subproject(s): H1/2

Abstract (click to open/close)

In preemptive real-time systems, scheduling analyses are based on the worst- case response time of tasks. This response time includes worst-case execution time (WCET) and context switch costs. In case of preemption, cache memories may suffer interferences between memory accesses of the preempted and of the preempting task. These interferences lead to some additional reloads that are referred to as cache-related preemption delay (CRPD). This CRPD constitutes a large part of the context switch costs. In this article, we focus on the computation of upper bounds on the CRPD using the concept of useful cache blocks (UCB). These are memory blocks that may be in cache before a program point and may be reused after it. When a preemption occurs at that point the number of additional cache-misses is bounded by the number of useful cache blocks. We tighten the CRPD bound by using a modified notion of UCB: Only cache blocks that are definitely cached are considered useful by our approach. As we show in this paper, the computed CRPD based on our notion, when used in combination with the bound on the WCET, delivers a safe bound on the execution time in case of preemption. Furthermore the modified definition simplifies the UCB computation for set-associative LRU and data caches. Experimental results show that our approach provides up to 90% tighter CRPD bounds.

Subproject(s): R2

Abstract (click to open/close)

Deferred preemption enables a trade-off between the high dynamics of a preemptive schedule on the one hand, and the predictability of a non- preemptive system on the other hand. In addition to bounds on the execution time and the context switch costs, the schedulability analysis for deferred preemption needs the maximum time a preemption can be delayed, also called maximum blocking time. Scheduling theory is based on an abstract level where these values are assumed to be given. So far, the computation of the maximum blocking time, however, has not been studied in detail. In this paper, we propose a new method to derive the maximum blocking time of a task given a fixed set of preemption points. To derive a safe upper bound, our approach also includes the context switch costs that might increase the maximum blocking time.

Subproject(s): R2

Abstract (click to open/close)

We present an approach to automatically generating invariants for timed automata models. The CIPM algorithm that we propose first computes new invariants for timed automata control locations taking their originally defined invariants as well as the constrains on clock variables imposed by incoming state transitions into account. In doing so the CIPM algorithm also prunes idle transitions, which are transitions that can never be taken, from the automaton. We discsuss a prototype implementation of the CIPM algorithm as well as some initial experimental results.

Subproject(s): R3

Subproject(s): R3

Abstract (click to open/close)

Non-determinism arises naturally in many real-world applications of action planning. Strong plans for this type of problems can be found using AO* search guided by an appropriate heuristic function. Most domain-independent heuristics considered in this context so far are based on the idea of ignoring delete lists and do not properly take the non-determinism into account. Therefore, we investigate the applicability of pattern database (PDB) heuristics to non-deterministic planning. PDB heuristics have emerged as rather informative in a deterministic context. Our empirical results suggest that PDB heuristics can also perform reasonably well in non-deterministic planning. Additionally, we present a generalization of the pattern additivity criterion known from classical planning to the non-deterministic setting.

Subproject(s): S1

Abstract (click to open/close)

Many heuristic estimators for classical planning are based on the so-called delete relaxation, which ignores negative effects of planning operators. Ideally, such heuristics would compute the actual goal distance in the delete relaxation, i.e., the cost of an optimal relaxed plan, denoted by h+. However, current delete relaxation heuristics only provide (often inadmissible) estimates to h+ because computing the correct value is an NP-hard problem. In this work, we consider the approach of planning with the actual h+ heuristic from a theoretical and computational perspective. In particular, we provide domain-dependent complexity results that classify some standard benchmark domains into ones where h+ can be computed efficiently and ones where computing h+ is NP-hard. Moreover, we study domain-dependent implementations of h+ which show that the h+ heuristic provides very informative heuristic estimates compared to other state-of-the-art heuristics.

Subproject(s): S1

Abstract (click to open/close)

Software and system dependability is getting ever more important in embedded system design. Current industrial practice of model-based analysis is supported by state-transition diagrammatic notations such as Statecharts. State-of-the-art modelling tools like STATEMATE support safety and failure-effect analysis at design time, but restricted to qualitative properties. This paper reports on a (plug-in) extension of STATEMATE enabling the evaluation of quantitative dependability properties at design time. The extension is compositional in the way the model is augmented with probabilistic timing information. This fact is exploited in the construction of the underlying mathematical model, a uniform continuous-time Markov decision process, on which we are able to check requirements of the form: "The probability to hit a safety-critical system configuration within a mission time of 3 hours is at most 0.01." We give a detailed explanation of the construction and evaluation steps making this possible, and report on a nontrivial case study of a high-speed train signalling system where the tool has been applied successfully.

Keywords: checking, ctmc, mdp, model, stochastic
Subproject(s): S3

Abstract (click to open/close)

Probabilistic model checking has emerged as a versatile system verification approach, but is frequently facing state-space explosion problems. One promising attack to this is to construct an abstract model which simulates the original model, and to perform model checking on that abstract model. Recently, efficient algorithms and optimizations for deciding simulation of probabilistic models have been proposed, which reduces the theoretical complexity bounds of existing algorithm drastically. In this paper we present a tool to compare the performance of these approaches for deciding the simulation preorder of probabilistic models.

Subproject(s): S3

Abstract (click to open/close)

Analysis and verification of safety critical systems is inevitable to assure functional and temporal correctness. For checking temporal system behaviour, real-time scheduling analysis has been proved to be an efficient method. As an analytical method, real-time scheduling relies on rather simple task network models mostly ignoring functional behaviour in order to remain computable and efficient. Functional and temporal system behaviour however are often closely related. By abstracting from functional behaviour, scheduling analysis often results in large over-approximation for such systems. We propose a task network model providing extensions to describe also functional system behaviour. The main elements are explicit data objects and tasks with internal states and data dependant executions. Since there are no analytical methods known to be available for such extended models we propose an analysis based on a combination of model-checking and testing. Although this technique does not provide exhaustive verification, it is a first step towards time-accurate analysis of complex real-time systems. Moreover, the approach provides a convenient way to check systems against functional and temporal requirements in contrast to analytical methods that are usually restricted to simple temporal properties like deadlines.

Subproject(s): R2

Abstract (click to open/close)

In preemptive real-time systems, scheduling analyses need--in addition to the worst-case execution time--the context-switch cost. In case of preemption, the preempted and the preempting task may interfere on the cache memory. These interferences lead to additional reloads in the preempted task. The delay due to these reloads is referred to as the cache-related preemption delay (CRPD). The CRPD constitutes a large part of the context-switch cost. In this article, we focus on the computation of upper bounds on the CRPD based on the concepts of useful cache blocks (UCBs) and evicting cache blocks (ECBs). We explain how these concepts can be used to bound the CRPD in case of direct-mapped caches. Then we consider set-associative caches with LRU, FIFO, and PLRU replacement. We show potential pitfalls when using UCBs and ECBs to bound the CRPD in case of LRU and demonstrate that neither UCBs nor ECBs can be used to bound the CRPD in case of FIFO and PLRU. Finally, we sketch a new approach to circumvent these limitations by using the concept of relative competitiveness.

Subproject(s): R2

Abstract (click to open/close)

Recently, Helmert and Geffner proposed the context-enhanced additive heuristic, where fact costs are evaluated relative to context states that arise from achieving first a pivot condition of each operator. As Helmert and Geffner pointed out, the method can be generalized to consider contexts arising from arbitrary precedence constraints over operator conditions instead. Herein, we provide such a generalization. We extend Helmert and Geffner's equations, and discuss a number of design choices that arise. Drawing on previous work on goal orderings, we design a family of methods for automatically generating precedence constraints. We run large-scale experiments, showing that the technique can help significantly, depending on the choice of precedence constraints. We shed some light on this by profiling the behavior of all possible precedence constraints, using a sampling technique.

Subproject(s): S1

Abstract (click to open/close)

Acyclic phase-type distributions can be used to describe the time until a basic event in a fault tree occurs. We show in this paper that the top event of a fault tree built from such basic events is also acyclic phase-type distributed. We then apply a recently developed acyclic phase-type minimization algorithm to effectively combat the state-space explosion problem in a dynamic fault tree analysis.

Subproject(s): S3

Abstract (click to open/close)

Self-stabilization is an elegant way of realizing non-masking fault-tolerant systems. Sustained research over last decades has produced multiple self-stabilizing algorithms for many problems in distributed computing. In this paper, we present a framework to evaluate multiple self-stabilizing solutions under a fault model that allows intermittent transient faults. To that end, metrics to quantify the dependability of self-stabilizing systems are defined. It is also shown how to derive models that are suitable for probabilistic model checking in order to determine those dependability metrics. A heuristics-based method is presented to analyze counterexamples returned by a probabilistic model checker in case the system under investigation does not exhibit the desired degree of dependability. Based on the analysis, the self-stabilizing algorithm is subsequently refined.

Subproject(s): S3

Abstract (click to open/close)

Formal methods play an important role in the development of safety-critical systems. Their well-defined semantics can be employed for automatic formal system verification. Modelchecking, a well-established formal verification technique, is however often restricted to an abstract level due to complexity reasons. For example, checking temporal system behaviour with respect to hardware architectures and operating systems is often not possible. Real-time scheduling theory on the other hand provides efficient techniques for temporal analysis of real-world systems at architecture level. However, models used in real-time scheduling theory usually lack a semantics that is compatible to those used by formal specifications. This prevents to verify temporal system behaviour at the architecture level with the same formal methods. We present an approach that combines a timed automata representation of task networks and efficient scheduling analysis techniques. Based on existing task network formalisms we define a consistent timed automaton model, and a mapping between both formalisms. We prove that the mapping induces behavioural equivalence of the models. We show an application of the approach by verifying task networks against Live Sequence Charts (LSC).

Subproject(s): R2

Abstract (click to open/close)

A distributed system is fault-tolerant if it continues to perform correctly even when a subset of the processes becomes faulty. Fault-tolerance is highly desirable but often difficult to implement. In this paper, we investigate fault-tolerant synthesis, i.e., the problem of determining whether a given temporal specification can be implemented as a fault-tolerant distributed system. As in standard distributed synthesis, we assume that the specification of the correct behaviors is given as a temporal formula over the externally visible variables. Additionally, we introduce the fault-tolerance specification, a CTL* formula describing the effects and the duration of faults. If, at some point in time, a process becomes faulty, it becomes part of the external environment and its further behavior is only restricted by the fault-tolerance specification. This allows us to model a large variety of fault types. Our method accounts for the effect of faults on the values communicated by the processes, and, hence, on the information available to the non-faulty processes. We prove that for fully connected system architectures, i.e., for systems where each pair of processes is connected by a communication link, the fault-tolerant synthesis problem from CTL* specifications is 2EXPTIME-complete.

Subproject(s): S1

Abstract (click to open/close)

In directed model checking, the traversal of the state space is guided by an estimate of the distance from the current state to the nearest error state. This paper presents a distance-preserving abstraction for concurrent systems that allows one to compute an interesting estimate of the error distance without hitting the state explosion problem. Our experiments show a dramatic reduction both in the number of states explored by the model checker and in the total runtime.

Subproject(s): R3

Abstract (click to open/close)

In this paper we make a step towards an algorithm for the verification of hybrid systems that, on the one hand allows very general inputs (e.g., with non-linear ordinary differential equations), but on the other hand exploits the structure of those parts of the input that represent special cases (e.g., clocks). We show how to compute slices of parallel hyperplanes separating reachable from unreachable parts of the state space for a given abstraction of the input system, and demonstrate the usefulness of such slices within an abstraction refinement algorithm based on hyper-rectangles.

Subproject(s): H1/2

Abstract (click to open/close)

In this short paper, we summarize our approach to analyzing hybrid discrete-continuous systems by reduction to constraint solving paired with enclosure methods for sets of initial value problems of ordinary differential equations.

Keywords: hybrid discrete-continuous systems, verification, ordinary differential equations, constraint solving, PACS: 02.60.Lj, 02.70.-c, 89.75.-k
Subproject(s): H1/2

Abstract (click to open/close)

In the analysis of hybrid discrete-continuous systems, rich arithmetic constraint formulae with complex Boolean structure arise naturally. The iSAT algorithm, a solver for such formulae, is aimed at bounded model checking of hybrid systems. In this paper, we identify challenges emerging from planned and ongoing work to enhance the iSAT algorithm. First, we propose an extension of iSAT to directly handle ordinary differential equations as constraints. Second, we outline the recently introduced generalization of the iSAT algorithm to deal with probabilistic hybrid systems and some open research issues in that context. Third, we present ideas on how to move from bounded to unbounded model checking by using the concept of interpolation. Finally, we discuss the adaption of some parallelization techniques to the iSAT case, which will hopefully lead to performance gains in the future. By presenting these open research questions, this paper aims at fostering discussions on these extensions of constraint solving.

Keywords: mixed Boolean and arithmetic constraints - differential equations - stochastic SMT - Craig interpolation - parallel solver
Subproject(s): H1/2

Subproject(s): H1/2

Abstract (click to open/close)

Planning systems for real-world applications need the ability to handle concurrency and numeric fluents. Nevertheless, the predominant approach to cope with concurrency followed by the most successful participants in the latest International Planning Competitions (IPC) is still to find a sequential plan that is rescheduled in a post-processing step. We present Temporal Fast Downward (TFD), a planning system for temporal problems that is capable of finding low-makespan plans by performing a heuristic search in a temporal search space. We show how the context-enhanced additive heuristic can be successfully used for temporal planning and how it can be extended to numeric fluents. TFD often produces plans of high quality and, evaluated according to the rating scheme of the last IPC, outperforms all state-of-the-art temporal planning systems.

Subproject(s): S1

Abstract (click to open/close)

We introduce a new conceptual approach of Verification Architectures that uses formally defined design patterns for complex real-time systems to facilitate decomposional verification of large systems. To this end, we provide an extension of CSP by data and undefined processes that allow us to specify Verification Architectures, i.e., abstract protocols with additional local assumptions in a real-time logic. We embedded our CSP extension into dynamic logic and define a sequent calculus to prove desired properties of those protocols. With a case study from the railway domain, we show that a Verification Architecture proven correct with our calculus helps us verify large systems decompositionally that are too complex for direct verification.

Subproject(s): R1

Abstract (click to open/close)

Synthesizing monitor circuits for LTL formulas is expensive, because the number of flip-flops in the circuit is exponential in the length of the formula. As a result, the IEEE standard PSL recommends to restrict monitoring to the simple subset and use the full logic only for static verification. We present a novel construction for the synthesis of monitor circuits from specifications in LTL. In our construction, only subformulas with unbounded-future operators contribute to the exponential blowup. We split the specification into a bounded and an unbounded part, apply specialized constructions for each part, and then compose the results into a monitor for the original specification. Since the unbounded part in practical specifications is often very small, we argue that, with the new construction, it is no longer necessary to restrict runtime verification to the simple subset.

Subproject(s): R1

Abstract (click to open/close)

Duration Calculus (abbreviated to DC) is an interval-based, metric-time temporal logic designed for reasoning about embedded real-time systems at a high level of abstraction. But the complexity of model checking any decidable fragment featuring both negation and chop, DC’s only modality, is non-elementary and thus impractical. Even worse, when such decidable fragments are generalized just slightly to cover more interesting durational constraints the resulting fragments become undecidable. We here investigate a similar approximation as frequently employed in model checking situation- or point-based temporal logics, where linear-time problems are safely approximated by branching-time counterparts amenable to more efficient model-checking algorithms. Mimicking the role that a situation has in (A)CTL as the origin of a set of linear traces, we define a branching-time counterpart to interval-based temporal logics building on situation pairs spanning sets of intervals. While this branching-time interval semantics yields the desired reduction in complexity of the model-checking problem, from undecidable to linear in the size of the formula and cubic in the size of the model, the approximation is too coarse to be practical. We therefore refine the semantics by an occurrence count for crucial states (e.g., cuts of loops) in the model, arriving at a 4-fold exponential model-checking problem sufficiently accurately approximating the original one. Furthermore, when chop occurs in negative polarity only in DC formulas, we have a doubly exponential model-checking algorithm.

Subproject(s): R1

Abstract (click to open/close)

We investigate the optimum reachability problem for Multi-Priced Timed Automata (MPTA) that admit both positive and negative costs on edges and locations, thus bridging the gap between the results of Bouyer et al. (2007) and of Larsen and Rasmussen (2008). Our contributions are the following: (1) We show that even the location reachability problem is undecidable for MPTA equipped with both positive and negative costs, provided the costs are subject to a bounded budget, in the sense that paths of the underlying Multi-Priced Transition System (MPTS) that operationally exceed the budget are considered as not being viable. This undecidability result follows from an encoding of Stop- Watch Automata using such MPTA, and applies to MPTA with as few as two cost variables, and even when no costs are incurred upon taking edges. (2) We then restrict the MPTA such that each viable quasi-cyclic path of the underlying MPTS incurs a minimum absolute cost. Under such a condition, the location reachability problem is shown to be decidable and the optimum cost is shown to be computable for MPTA with positive and negative costs and a bounded budget. These results follow from a reduction of the optimum reachability problem to the solution of a linear constraint system representing the path conditions over a finite number of viable paths of bounded length.

Subproject(s): R1

Subproject(s): H1/2

Abstract (click to open/close)

In hard real-time systems, the execution time of programs must be bounded by static timing analysis. For today's embedded systems featuring caches, static analyses must predict cache hits and misses with high precision to obtain useful bounds. For caches with least-recentlyused (LRU) replacement policy, editorcient and precise cache analyses exist. However, for other widely-used policies like rst-in rst-out (FIFO), current cache analyses are much less precise. This paper discusses challenges in FIFO cache analysis and advances the state of the art. We identify a generic framework for cache analysis that couples may- and must-analyses by means of domain cooperation. Our main contribution is a more precise may-analysis for FIFO. It not only increases the number of predicted misses, but also|due to the domain cooperation|the number of predicted hits.We instantiate the framework with a canonical must-analysis and three dirent may-analyses, including our new one, and compare the resulting three analyses to the collecting semantics. Our evaluation results characterize the progress achieved by our new may-analysis and reveal room for further improvement.

Subproject(s): R2

Abstract (click to open/close)

One step in the verification of hard real-time systems is to determine upper bounds on the worst-case execution times (WCET) of tasks. To obtain tight bounds, a WCET analysis has to consider microarchitectural features like caches, branch prediction, and branch target buffers (BTB). We propose a modular WCET analysis framework for branch target buffers (BTB), which allows for easy adaptability to different BTBs. As an example, we investigate the MOTOROLA POWERPC 56X family (MPC56X), which is used in automotive and avionic systems. On a set of avionic and compiler benchmarks, our analysis improves WCET bounds on average by 13% over no BTB analysis. Capitalizing on the modularity of our framework, we explore alternative hardware designs. We propose more predictable designs, which improve obtainable WCET bounds by up to 20%, reduce analysis time considerably, and simplify the analysis. We generalize our findings and give advice concerning hardware used in real-time systems.

Subproject(s): R2

Abstract (click to open/close)

There is a growing interest in research related to presenting correct and efficient model checking approaches for complex computing systems. Abstraction model checking is one example which proved its success as a model checking approach for infinite-state systems. In this thesis, we present an approach for translating CSP-OZ-DC specifications into transition constraint systems (as a part of a model checking approach for infinite-state systems). In previous works, the CSP-OZ-DC specifications are translated into phase event automata, then, the product of the phase event automata is translated into a transition constraint system. For large specifications, the obtained transition constraint system can result in a large number of transitions. In our approach, we provide an improved representation of transition constraint systems consisting of a notably lower number of transitions in the transition constraint system with the aim of achieving faster model checking for available model-checkers.

Subproject(s): R1

Abstract (click to open/close)

The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are a widely used modeling formalism that captures such performance and dependability properties and makes them analyzable by model checking. In this paper, we focus on probabilistic timing properties of infinite-state CTMCs, expressible in continuous stochastic logic (CSL). This comprises important dependability measures, such as timed probabilistic reachability, performability, survivability, and various availability measures like instantaneous, conditional instantaneous and interval availabilities. Conventional model checkers explore the given model exhaustively, which is often costly, due to state explosion, and sometimes impossible because the model is infinite. This paper presents a method that only explores the model up to a finite depth, with the depth bound being computed on the fly. The computation of depth bounds is configurable to adapt to the characteristics of different classes of models. We provide experimental evidence showing that our method is effective.

Subproject(s): S3

Abstract (click to open/close)

The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are a widely used modeling formalism that captures such performance and dependability properties, and makes them analyzable by model checking. In this paper, we focus on time-bounded probabilistic properties of infinite-state CTMCs, expressible in a subset of continuous stochastic logic (CSL). This comprises important dependability measures, such as time-bounded probabilistic reachability, performability, survivability, and various availability measures like instantaneous, conditional instantaneous and interval avail- abilities. Conventional model checkers explore the given model exhaustively, which is often costly, due to state explosion, and sometimes impossible because the model is infinite. This paper presents a method that only explores the model up to a finite depth. The required depth is determined on the fly by an algorithm that is configurable in order to adapt to the characteristics of different classes of models. We provide experimental evidence showing that our method is effective.

Subproject(s): S3

Abstract (click to open/close)

The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are a widely used modeling formalism, where performance and dependability properties are analyzable by model checking. We present INFAMY, a model checker for arbitrarily structured infinite-state CTMCs. It checks probabilistic timing properties expressible in continuous stochastic logic (CSL). Conventional model checkers explore the given model exhaustively, which is often costly, due to state explosion, and impossible if the model is infinite. INFAMY only explores the model up to a finite depth, with the depth bound being computed on-the-fly. The computation of depth bounds is configurable to adapt to the characteristics of different classes of models.

Subproject(s): S3

Abstract (click to open/close)

Given a parametric Markov model, we consider the problem of computing the rational function expressing the probability of reaching a given set of states. To attack this principal problem, Daws has suggested to first convert the Markov chain into a finite automaton, from which a regular expression is computed. Afterwards, this expression is evaluated to a closed form function representing the reachability probability. This paper investigates how this idea can be turned into an effective procedure. It turns out that the bottleneck lies in the growth of the regular expression relative to the number of states (n ^{Theta ( log n)}). We therefore proceed differently, by tightly intertwining the regular expression computation with its evaluation. This allows us to arrive at an effective method that avoids this blow up in most practical cases. We give a detailed account of the approach, also extending to parametric models with rewards and with non-determinism. Experimental evidence is provided, illustrating that our implementation provides meaningful insights on non-trivial models.

Subproject(s): S3

Abstract (click to open/close)

Given a parametric Markov model, we consider the problem of computing the rational function expressing the probability of reaching a given set of states. To attack this principal problem, Daws has suggested to first convert the Markov chain into a finite automaton, from which a regular expression is computed. Afterwards, this expression is evaluated to a closed form function representing the reachability probability. This paper investigates how this idea can be turned into an effective procedure. It turns out that the bottleneck lies in the growth of the regular expression relative to the number of states (n ^{Theta ( log n)}). We therefore proceed differently, by tightly intertwining the regular expression computation with its evaluation. This allows us to arrive at an effective method that avoids this blow up in most practical cases. We give a detailed account of the approach, also extending to parametric models with rewards and with non-determinism. Experimental evidence is provided, illustrating that our implementation provides meaningful insights on non-trivial models.

Subproject(s): S3

Abstract (click to open/close)

The formalism of probabilistic timed automata (PTA) combines discrete probabilities, time and nondeterminism. We developed mcpta, a fully automatic model-checking tool for PTA specified in Modest, a high-level compositional modelling language that includes features such as exception handling, dynamic parallelism and recursion. It uses an integral semantics for time, representing clocks with bounded integer variables, which makes it possible to use established probabilistic model-checking tools for the analysis. The use of Modest allows models to be specified in a convenient, succinct fashion while support for certain forms of dynamic parallelism simplifies modularisation. In order to cope with large systems, mcpta optimises the models, leading to significant reductions in terms of state-space and model-checking times in the case studies we considered. In this report, we investigate the relationship between Modest and PTA, show how to correctly transform a large subset of Modest including a form of dynamic parallelism for use with the probabilistic model-checker PRISM, and present the tool implementation and its application to several case-studies, highlighting performance improvements due to automatic optimisation as well as elegant modelling techniques made possible by exploiting Modest language features.

Subproject(s): S2

Abstract (click to open/close)

Probabilistic timed automata (PTA) combine discrete probabilistic choice, real time and nondeterminism. This paper presents a fully automatic tool for model checking PTA with respect to probabilistic and expected reachability properties. PTA are specified in Modest, a high-level compositional modelling language that includes features such as exception handling, dynamic parallelism and recursion, and thus enables model specification in a convenient fashion. For model checking, we use an integral semantics of time, representing clocks with bounded integer variables. This makes it possible to use the probabilistic model checker PRISM as analysis backend. We describe details of the approach and its implementation, and report results obtained for three different case studies.

Subproject(s): S2

Subproject(s): R1

Abstract (click to open/close)

We present a new counterexample-guided abstraction refinement scheme. The scheme refines an over-approximation of the set of possible traces. Each refinement step introduces a finite automaton that recognizes a set of infeasible traces. A central idea enabling our approach is to use interpolants (assertions generated, e.g., by the infeasibility proof for an error trace) in order to automatically construct such an automaton. A data base of interpolant automata has an interesting potential for reuse of theorem proving work (from one program to another).

Subproject(s): R1

Abstract (click to open/close)

We introduce an efficient method for translating planning tasks specified in the standard PDDL formalism into a concise grounded representation that uses finite-domain state variables instead of the straight-forward propositional encoding. Translation is performed in four stages. Firstly, we transform the input task into an equivalent normal form expressed in a restricted fragment of PDDL. Secondly, we synthesize invariants of the planning task that identify groups of mutually exclusive propositions which can be represented by a single finite-domain variable. Thirdly, we perform an efficient relaxed reachability analysis using logic programming techniques to obtain a grounded representation of the input. Finally, we combine the results of the third and fourth stage to generate the final grounded finite-domain representation. The presented approach has originally been implemented as part of the Fast Downward planning system for the 4th International Planning Competition (IPC4). Since then, it has been used in a number of other contexts with considerable success, and the use of concise finite-domain representations has become a common feature of state-of-the-art planners.

Subproject(s): S1

Abstract (click to open/close)

Current heuristic estimators for classical domain-independent planning are usually based on one of four ideas: delete relaxations, critical paths, abstractions, and, most recently, landmarks. Previously, these different ideas for deriving heuristic functions were largely unconnected. We prove that admissible heuristics based on these ideas are in fact very closely related. Exploiting this relationship, we introduce a new admissible heuristic called the landmark cut heuristic, which compares favourably with the state of the art in terms of heuristic accuracy and overall performance.

Subproject(s): S1

Abstract (click to open/close)

In this thesis we discuss the verification of systems to guarantee their correct behavior, that is given by a specification, using formal techniques. For the work at hand, the mathematical and algorithmic methods that are used for this verification task are the application of the so-called model checking technique that is combined with automated proof systems for solving the satisfiability problem (short: SAT). SAT-based verification of circuits and discrete systems has become one of the most effective technique within the last 10 years, such that industrial as well as academic applications heavily rely on it. SAT-based verification is the topic of this thesis, too, whereby our contributions cover the whole range of a SAT-based tool application. This means in practical terms that we propose extensions and concepts that concentrate on the core of a SAT-solver. However, these proposals are then transfered to novel verification models such as linear hybrid automata. Furthermore, we describe and evaluate approaches that incorporate the structure of the underlying problem to exploit knowledge gained during the verification process on the level of the SAT-solver. The main focus of the thesis at hand is on the verification of incomplete system designs, which occur for example in the early phase of a design. Our contributions are several SAT-based modeling techniques for the verification of such incomplete system designs. We describe various modeling concepts that can be embedded into a taxonomy with respect to their expressiveness and required computational resources, such that depending on the complexity of the underlying verification problem different methods are available, thus assuring a flexible approach for the desired verification. The proposed methods are evaluated experimentally to guarantee their applicability in practice. Taken together, this thesis provides contributions to the state-of-the-art in SAT-based verification, starting from core algorithms up to novel application domains.

Subproject(s): S1

Abstract (click to open/close)

Thanks to recent advances, AI Planning has become the underlying technique for several applications. Figuring prominently among these is automated Web Service Composition (WSC) at the "capability" level, where services are described in terms of preconditions and effects over ontological concepts. A key issue in addressing WSC as planning is that ontologies are not only formal vocabularies; they also axiomatize the possible relationships between concepts. Such axioms correspond to what has been termed "integrity constraints" in the actions and change literature, and applying a web service is essentially a belief update operation. The reasoning required for belief update is known to be harder than reasoning in the ontology itself. The support for belief update is severely limited in current planning tools. Our first contribution consists in identifying an interesting special case of WSC which is both significant and more tractable. The special case, which we term forward effects, is characterized by the fact that every ramification of a web service application involves at least one new constant generated as output by the web service. We show that, in this setting, the reasoning required for belief update simplifies to standard reasoning in the ontology itself. This relates to, and extends, current notions of "message-based" WSC, where the need for belief update is removed by a strong (often implicit or informal) assumption of "locality" of the individual messages. We clarify the computational properties of the forward effects case, and point out a strong relation to standard notions of planning under uncertainty, suggesting that effective tools for the latter can be successfully adapted to address the former. Furthermore, we identify a significant sub-case, named strictly forward effects, where an actual compilation into planning under uncertainty exists. This enables us to exploit off-the-shelf planning tools to solve message-based WSC in a general form that involves powerful ontologies, and requires reasoning about partial matches between concepts. We provide empirical evidence that this approach may be quite effective, using Conformant-FF as the underlying planner.

Subproject(s): S1

Abstract (click to open/close)

Saturation-based calculi such as superposition can be successfully instantiated to decision procedures for many decidable fragments of first-order logic. In case of termination without generating an empty clause, a saturated clause set implicitly represents a minimal model for all clauses, based on the underlying term ordering of the superposition calculus. In general, it is not decidable whether a ground atom, a clause or even a formula holds in this minimal model of a satisfiable saturated clause set. We extend our superposition calculus for fixed domains with syntactic disequality constraints in a non-equational setting. Based on this calculus, we present several new decidability results for validity in the minimal model of a satisfiable finitely saturated clause set that in particular extend the decidability results known for ARM (Atomic Representations of term Models) and DIG (Disjunctions of Implicit Generalizations) model representations.

Subproject(s): H1/2

Abstract (click to open/close)

We present a new saturation-based decidability result for inductive validity. Let Sigma be a finite signature in which all function symbols are at most unary and let N be a satisfiable Horn clause set without equality in which all positive literals are linear. If N cup A_1,...,A_n -> belongs to a class that can be finitely saturated by ordered resolution modulo variants, then it is decidable whether a sentence of the form forall x exists y.A1 and ... and A_n is valid in the minimal model of N.

Subproject(s): H1/2

Abstract (click to open/close)

This system description provides an overview of H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions), a program for hierarchical reasoning in extensions of logical theories with functions axiomatized by a set of clauses. H-PILoT reduces deduction problems in the theory extension to deduction problems in the base theory. Specialized provers and standard SMT solvers can be used for testing the satisfiability of the formulae obtained after the reduction. For local theory extensions this hierarchical reduction is sound and complete and -- if the formulae obtained this way belong to a fragment decidable in the base theory -- H-PILoT provides a decision procedure for testing satisfiability of ground formulae, and can also be used for model generation.

Subproject(s): R1,H3

Abstract (click to open/close)

Many verification approaches use SMT solvers in some form, and are limited by their incomplete handling of quantified formulas. Local reasoning allows to handle SMT problems involving a certain class of universally quantified formulas in a complete way by instantiation to a finite set of ground formulas. We present a method to generate these instances incrementally, in order to provide a more efficient way of solving these satisfiability problems. The incremental instantiation is guided semantically, inspired by the instance generation approach to first-order theorem proving. Our method is sound and complete, and terminates on both satisfiable and unsatisfiable input after generating a subset of the instances needed in standard local reasoning. Experimental results show that for a large class of examples the incremental approach is substantially more efficient than eager generation of all instances.

Subproject(s): R1

Abstract (click to open/close)

This paper describes the Parallel Interval COnstraint SOlver Picoso, which can decide (a subclass of) boolean combinations of linear and non-linear constraints. Picoso follows a master/client model based on message passing, making it suitable for any kind of workstation cluster as well as for multi-processor machines. To run several clients in parallel, an efficient work stealing mechanism has been integrated, dividing the overall search space into disjoint parts. Additionally, to prevent the clients from running into identical conflicts, information about conflicts in form of conflict clauses is exchanged among the clients. Performance measurements, using four clients to solve a number of benchmark problems, show that Picoso yields linear speedup compared to the sequential interval constraint solver iSAT, on which the clients of Picoso are based.

Subproject(s): H1/2

Abstract (click to open/close)

The Markov Reward Model Checker (MRMC) is a software tool for verifying properties over probabilistic models. It supports PCTL and CSL model checking, and their reward extensions. Distinguishing features of MRMC are its support for computing time- and reward-bounded reachability probabilities, (property-driven) bisimulation minimization, and precise on-the-fly steady-state detection. Recent tool features include time-bounded reachability analysis for uniform CTMDPs and CSL model checking by discrete-event simulation. This paper presents the tool's current status and its implementation details.

Subproject(s): S3

Abstract (click to open/close)

We present an AC1(logDCFL) algorithm for checking LTL formulas over finite paths, thus establishing that the problem can be efficiently parallelized. Our construction provides a foundation for the parallelization of various applications in monitoring, testing, and verification.

Subproject(s): S1

Subproject(s): R3

Abstract (click to open/close)

Symbolic methods in computer-aided verification rely on appropriate constraint solvers. Correctness and reliability of solvers are a vital requirement in the analysis of safety-critical systems, e.g., in the automotive context. Satisfiability results of a solver can usually be checked by probing the computed solution. However, efficient validation of an uncertified unsatisfiability result for some constraint formula is nearly impossible. In this paper, we propose a certification method for unsatisfiability results for mixed Boolean and non-linear arithmetic constraint formulae. Such formulae arise in the analysis of hybrid discrete-continuous systems.

Subproject(s): H1/2

Abstract (click to open/close)

In this paper we present the parallel QBF Solver PaQuBE. This new solver leverages the additional computational power that can be exploited from modern computer architectures, from pervasive multicore boxes to clusters and grids, to solve more relevant instances and faster than previous generation solvers. PaQuBE extends QuBE, its sequential core, by providing a Master/Slave Message Passing Interface (MPI) based design that allows it to split the problem up over an arbitrary number of distributed processes. Furthermore, PaQuBE's progressive parallel framework is the first to support advanced knowledge sharing in which solution cubes as well as conflict clauses can be shared. According to the last QBF Evaluation, QuBE is the most powerful state-of-the-art QBF Solver. It was able to solve more than twice as many benchmarks as the next best independent solver. Our results here, show that PaQuBE provides additional speedup, solving even more instances, faster.

Subproject(s): S1

Abstract (click to open/close)

Safety-critical hard real time systems as the flight control computer in avionics or airbag control software in the automotive industry need to be validated for their correct behavior. Besides the functional correctness, timely task completion is essential, i.e. the worst-case execution time (WCET) of each task in the system has to be determined. Saarland University and AbsInt GmbH have successfully developed the aiT WCET analyzer for computing safe upper bounds on the WCET of a task. The computation is mainly based on abstract interpretation of timing models of the processor and its periphery. Such timing models are currently hand-crafted by human experts. Therefore their implementation is a time-consuming and error-prone process. This paper presents an abstraction-aware compiler for automatically generating efficient pipeline analyzes out of abstracted timing models that could be derived from formal VHDL specifications.

Subproject(s): R2

Abstract (click to open/close)

In this paper we examine the effect that different knowledge sharing strategies have on the performance of our parallel QBF Solver PaQuBE. This new Master/Slave MPI based solver leverages the additional computational power that can be exploited from modern computer and system architectures, to solve more relevant instances and faster than previous generation solvers. Knowledge sharing plays a critical role in the performance of PaQuBE. However, due to the overhead associated with sending and receiving MPI messages, and the restricted communication/network bandwidth available between solvers, it is essential that we optimize not only which information is shared, but how it is shared. In this context, we compare multiple conflict clause and solution cube sharing strategies, and finally show that an adaptive method works best. Additionally, compression of solution cubes was explored which reduced the system time associated with message passing while also reducing network traffic.

Subproject(s): S1

Abstract (click to open/close)

In this paper we examine the effect that different knowledge sharing strategies have on the performance of our parallel QBF Solver PaQuBE. This new Master/Slave MPI based solver leverages the additional computational power that can be exploited from modern computer and system architectures, to solve more relevant instances and faster than previous generation solvers. Knowledge sharing plays a critical role in the performance of PaQuBE. However, due to the overhead associated with sending and receiving MPI messages, and the restricted communication/network bandwidth available between solvers, it is essential that we optimize not only which information is shared, but how it is shared. In this context, we compare multiple conflict clause and solution cube sharing strategies, and finally show that an adaptive method works best. Additionally, compression of solution cubes was explored which reduced the system time associated with message passing while also reducing network traffic.

Subproject(s): S1

Abstract (click to open/close)

Black Box symbolic model checking is a method to check whether an incompletely specified circuit, in which some parts of the design have been replaced by Black Boxes, satisfies a CTL property regardless of the actual replacement of the Black Boxes. One possible application is model checking with abstraction where complex parts of the design (which are not really relevant for the property at hand) are put into Black Boxes in order to speed up the model checking run. However, due to its approximative nature, symbolic model checking for incomplete designs may be unable to provide proofs when the approximations are to coarse. In this paper we show how Black Box model checking can profit from information about the Black- Boxed parts given in form of so-called local component assumptions. The assumptions we use in this context are safety properties arguing about fixed time windows. Furthermore we will present a set of heuristic-based approaches to automatically select a subset of local component assumptions that is sufficient to prove or disprove a given CTL property.

Abstract (click to open/close)

What to do if at a given time a service dearly required is unavailable? Is it a good strategy to simply invoke the service again (and again)? How many times should one retry in such a situation in order to get a the service delivered with a reasonably high probability but without "losing too much time?" In this paper, we explore the relation between time redundancy that a system can utilize to cope with faults and the increase of system availability. We propose a generalization of instantaneous availability called instantaneous window availability to systematize our approach. We then present two methods for deriving trade-off solutions in terms of average instantaneous window availability, namely Markov model analysis and discrete-time simulation. We apply these methods to two instances of a self-stabilizing system and discuss the outcome.

Keywords: Availability, Self-Stabilization, Fault Tolerance, Prism, Simulation, SiSSDA, Limiting Window Availability
Subproject(s): S3

Abstract (click to open/close)

In this paper, we present an automatable decompositional method for the computation of Lyapunov functions for hybrid systems with complex discrete state spaces. We use graph-based reasoning to decompose hybrid automata into subgraphs, for which we then solve semidefinite optimization problems to obtain local Lyapunov functions. These local computations are made in a way that ensures that the family of local Lyapunov functions forms a global Lyapunov function, proving asymptotic stability of the system. The main advantages over standard LMI methods are 1) improved numerical stability due to smaller optimization problems, 2) the possibility of incremental construction of stable hybrid automata and 3) easier diagnosis of unstable parts of the automaton in case no Lyapunov function can be found.

Subproject(s): H4

Abstract (click to open/close)

In this paper, we describe a decompositional approach to convergence proofs for stochastic hybrid systems given as probabilistic hybrid automata. We focus on a concept called "stability in probability," which implies convergence of almost all trajectories of the stochastic hybrid system to a designated equilibrium point. By adapting classical Lyapunov function results to the stochastic hybrid case, we show how automatic stability proofs for such systems can be obtained with the help of numerical tools. To ease the load on the numerical solvers and to permit incremental construction of stable systems, we then propose an automatable Lyapunov-based decompositional framework for stochastic stability proofs. This framework allows conducting sub-proofs separately for different parts of the automaton, such that they still yield a proof for the entire system. Finally, we give an outline on how these decomposition results can be applied to conduct quantitative probabilistic convergence analysis, i.e., determining convergence probabilities below 1.

Subproject(s): H4

Abstract (click to open/close)

We present a novel technique for synthesizing controllers for distributed real-time environments with safety requirements. Our approach is an abstraction refinement extension to the on-the-fly algorithm by Cassez et al. from 2005. Based on partial compositions of some environment components, each refinement cycle constructs a sound abstraction that can be used to obtain under- and over-approximations of all valid controller implementations. This enables (1) early termination if an implementation does not exist in the over-approximation, or, if one does exist in the under-approximation, and (2) pruning of irrelevant moves in subsequent refinement cycles. In our refinement loop, the precision of the abstractions incrementally increases and converges to all specification-critical components. We implemented our approach in a prototype synthesis tool and evaluated it on an industrial benchmark. In comparison with the timed game solver UPPAAL-Tiga, our technique outperforms the nonincremental approach by an order of magnitude.

Subproject(s): R3,S1

Abstract (click to open/close)

In this paper we present a procedure for solving quantified boolean formulas (QBF), which uses And-Inverter Graphs (AIGs) as the core data-structure. We make extensive use of structural information extracted from the input formula such as functional definitions of variables and non-linear quantifier structures. We show how this information can directly be exploited by the symbolic, AIG based representation. We implemented a prototype QBF solver based on our ideas and performed a number of experiments proving the effectiveness of our approach, and moreover, showing that our method is able to solve QBF instances on which state-of-the-art QBF solvers known from literature fail.

Subproject(s): S1

Abstract (click to open/close)

We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose right-hand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. With this compositional approach we exploit locality in system designs. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control and car control.

Keywords: verification of hybrid systems, differential invariants, verification logic, fixedpoint engine
Subproject(s): H3

Abstract (click to open/close)

Complex physical systems have several degrees of freedom. They only work correctly when their control parameters obey corresponding constraints. Based on the informal specification of the European Train Control System (ETCS), we design a controller for its cooperation protocol. For its free parameters, we successively identify constraints that are required to ensure collision freedom. We formally prove the parameter constraints to be sharp by characterizing them equivalently in terms of reachability properties of the hybrid system dynamics. Using our deductive verification tool KeYmaera, we formally verify controllability, safety, liveness, and reactivity properties of the ETCS protocol that entail collision freedom. We prove that the ETCS protocol remains correct even in the presence of perturbation by disturbances in the dynamics. Finally we verify that safety is preserved when a PI controller is used for speed supervision.

Subproject(s): H3

Abstract (click to open/close)

Complex physical systems have several degrees of freedom. They only work correctly when their control parameters obey corresponding constraints. Based on the informal specification of the European Train Control System (ETCS), we design a controller for its cooperation protocol. For its free parameters, we successively identify constraints that are required to ensure collision freedom. We formally prove the parameter constraints to be sharp by characterizing them equivalently in terms of reachability properties of the hybrid system dynamics. Using our deductive verification tool KeYmaera, we formally verify controllability, safety, liveness, and reactivity properties of the ETCS protocol that entail collision freedom. We prove that the ETCS protocol remains correct even in the presence of perturbation by disturbances in the dynamics. Finally we verify that safety is preserved when a PI controller is used for speed supervision.

Subproject(s): H3

Abstract (click to open/close)

Scalable handling of real arithmetic is a crucial part ofthe verification of hybrid systems, mathematical algorithms, and mixedanalog/digital circuits. Despite substantial advances inverification technology, complexity issues with classical decisionprocedures are still a major obstacle for formal verification ofreal-world applications, e.g., in automotive and avionicindustries. To identify strengths and weaknesses, we examine stateof the art symbolic techniques and implementations for theuniversal fragment of real-closed fields: approaches based onquantifier elimination, Gröbner Bases, and semidefiniteprogramming for the Positivstellensatz. Within a uniform contextof the verification tool KeYmaera, we compare these approachesqualitatively and quantitatively on verification benchmarks fromhybrid systems, textbook algorithms, and on geometric problems.Finally, we introduce a new decision procedure combiningGröbner Bases and semidefinite programming for the realNullstellensatz that outperforms the individual approaches on aninteresting set of problems.

Subproject(s): H3

Abstract (click to open/close)

Scalable handling of real arithmetic is a crucial part of the verification of hybrid systems, mathematical algorithms, and mixed analog/digital circuits. Despite substantial advances in verification technology, complexity issues with classical decision procedures are still a major obstacle for formal verification of real-world applications, e.g., in automotive and avionic industries. To identify strengths and weaknesses, we examine state of the art symbolic techniques and implementations for the universal fragment of real-closed fields: approaches based on quantifier elimination, Gröbner Bases, and semidefinite programming for the Positivstellensatz. Within a uniform context of the verification tool KeYmaera, we compare these approaches qualitatively and quantitatively on verification benchmarks from hybrid systems, textbook algorithms, and on geometric problems. Finally, we introduce a new decision procedure combining Gröbner Bases and semidefinite programming for the real Nullstellensatz that outperforms the individual approaches on an interesting set of problems.

Subproject(s): H3

Abstract (click to open/close)

Acyclic phase-type distributions are phase-type distributions with triangular matrix representations. They constitute a versatile modelling tool in many circumstances. The size of their matrix representation has a strong influence on computational efforts needed when analyzing these distributions. This representation, however, is not unique, and two representations of the same distribution can differ drastically in size. This paper explores an effective algorithm to reduce the size of the matrix representation without altering the distribution. This proceeds via a symbolic representation of the Laplace-Stieltjes transform of the phase-type distribution. The algorithm is of cubic complexity in the size of the given representation. We clarify the circumstances under which the algorithm returns a minimal representation, and discuss in how far it can keep representations minimal when they are constructed via any of three operations--convolution, minimum, and maximum. A case study modelling delay propagation in railway networks demonstrates the practicality of the approach.

Subproject(s): S3

Abstract (click to open/close)

We study time-bounded reachability in continuous-time Markov decision processes for various scheduler classes. Such reachability problems play a paramount role in dependability analysis and the modelling of manufacturing and queueing systems. Consequently, their analysis has been studied intensively, and techniques for the approximation of optimal control are well understood. From a mathematical point of view, however, the question of approximation is secondary compared to the fundamental question whether or not optimal control exists. We demonstrate the existence of optimal schedulers for all commonly considered scheduler classes. For scheduler classes without full access to time we provide an effective technique to determine simple optimal schedulers that converge to an easy-to-compute memoryless scheduling policy after a finite number of steps.

Subproject(s): S1

Abstract (click to open/close)

We present an algorithm for falsifying safety properties of hybrid systems, i.e., for finding a trajectory to an unsafe state. The approach is to approximate how close a point is to being an initial point of an error trajectory using a real-valued quality function, and then to use numerical optimisation to search for an optimum of this function. The function is computed by running simulations, where information coming from abstractions computed by a verification algorithm is exploited to determine whether a simulation looks promising and should be continued or cancelled. This information becomes more reliable as the abstraction becomes more refined. We thus interleave falsification and verification attempts. In contrast to related work, we consider hybrid systems with completely deterministic evolution.

Subproject(s): H1/2

Abstract (click to open/close)

We present an algorithm for falsifying safety properties of hybrid systems, i.e., for finding a trajectory to an unsafe state. The approach is to approximate how close a point is to being an initial point of an error trajectory using a real-valued quality function, and then to use numerical optimisation to search for an optimum of this function. The function is computed by running simulations, where information coming from abstractions computed by a verification algorithm is exploited to determine whether a simulation looks promising and should be continued or cancelled. This information becomes more reliable as the abstraction becomes more refined. We thus interleave falsification and verification attempts.

Subproject(s): H1/2

Abstract (click to open/close)

Heuristic forward search is the dominant approach to satisficing planning to date. Most successful planning systems, however, go beyond plain heuristic search by employing various search-enhancement techniques. One example is the use of helpful actions or preferred operators, providing information which may complement heuristic values. A second example is deferred heuristic evaluation, a search variant which can reduce the number of costly node evaluations. Despite the wide-spread use of these search-enhancement techniques however, we note that few results have been published examining their usefulness. In particular, while various ways of using, and possibly combining, these techniques are conceivable, no work to date has studied the performance of such variations. In this paper, we address this gap by examining the use of preferred operators and deferred evaluation in a variety of settings within best-first search. In particular, our findings are consistent with and help explain the good performance of the winners of the satisficing tracks at IPC 2004 and 2008.

Subproject(s): S1

Abstract (click to open/close)

Interpolation is an important component of recent methods for program verification. It provides a natural and effective means for computing separation between the sets of `good' and `bad' states. The existing algorithms for interpolant generation are proof-based: They require explicit construction of proofs, from which interpolants can be computed. Construction of such proofs is a difficult task. We propose an algorithm for the generation of interpolants for the combined theory of linear arithmetic and uninterpreted function symbols that does not require a priori constructed proofs to derive interpolants. It uses a reduction of the problem to constraint solving in linear arithmetic, which allows application of existing highly optimized Linear Programming solvers in black-box fashion. We provide experimental evidence of the practical applicability of our algorithm.

Subproject(s): R1

Abstract (click to open/close)

We present a method which computes optimized representations for non-convex polyhedra. Our method detects so-called redundant linear constraints in these representations by using an incremental SMT (Satisfiability Modulo Theories) solver and then removes the redundant constraints based on Craig interpolation. The approach is motivated by applications in the context of model checking for Linear Hybrid Automata. Basically, it can be seen as an optimization method for formulas including arbitrary boolean combinations of linear constraints and boolean variables. We show that our method provides an essential step making quantifier elimination for linear arithmetic much more efficient. Experimental results clearly show the advantages of our approach in comparison to state-of-the-art solvers.

Subproject(s): H3

Abstract (click to open/close)

This article describes PaMiraXT, a powerful parallel SAT algorithm. PaMiraXT follows a master/client model based on message passing, making it suitable for any kind of workstation cluster. For the clients, MiraXT is used, which itself is thread-based parallel solver designed to take advantage of current and future shared memory multiprocessor systems. We highlight design and implementation details that allow the threads/clients to run and cooperate efficiently. Experimental results show that MiraXT compares well to other state-of-the-art SAT algorithms. In single-threaded mode, it outperforms MiniSat2, PicoSAT 535, and RSat 2.01, while in multi-threaded mode, MiraXT provides cutting edge performance, as it solves significantly more instances within the given time limit. A case study, using three copies of MiraXT with a total of 8 threads as clients, underlines the potential of PaMiraXT, resulting in a speedup of 5.62 on the industrial benchmarks of the 2007 SAT competition.

Subproject(s): H1,H2

Subproject(s): S2

Abstract (click to open/close)

In artificial intelligence, a relaxation of a problem is an overapproximation whose solution in every state of an explicit search provides a heuristic solution distance estimate. The heuristic guides the exploration, potentially shortening the search by exponentially many search states. The big question is how a good relaxation for the problem at hand should be derived. In model checking, overapproximations are called abstractions, and abstraction refinement is a powerful method developed to derive approximations that are sufficiently precise for verifying the system at hand. In our work, we bring these two paradigms together. We pioneer the application of (predicate) abstraction refinement for the generation of heuristic functions that are intelligently adapted to the problem at hand. We investigate how an abstraction refinement process for generating heuristic functions should differ from the process used in the verification context. We do so in the context of DMC of timed automata. We obtain a variety of interesting insights about this approach.

Subproject(s): R3

Abstract (click to open/close)

We study possibilities of reasoning about extensions of base theories with functions which satisfy certain recursion (or homomorphism) properties. Our focus is on emphasizing possibilities of hierarchical and modular reasoning in such extensions and combinations thereof. We present practical applications in verification and cryptography.

Subproject(s): R1

Abstract (click to open/close)

In this paper we show that states, transitions and behavior of concurrent systems can often be modeled as sheaves over a suitable topological space. In this context, geometric logic can be used to describe which local properties, of individual systems, are preserved, at a global level, when interconnecting the systems. The main area of application is to modular verification of complex systems. We illustrate our ideas by means of an example involving a family of interacting controllers for trains on a rail track.

Subproject(s): R1,H3

Abstract (click to open/close)

Aiming at fully symbolic methods for the analysis of probabilistic hybrid systems, we recently introduced the notion of stochastic satisfiability modulo theories (SSMT) problems and the corresponding SiSAT solving algorithm. The notion of SSMT extends SMT with randomized (aka. stochastic) as well as existential and universal quantification as known from stochastic propositional satisfiability. In this paper, we describe the symbolic encoding of scheduled-event probabilistic hybrid automata by means of a case study from the networked automation system domain. We furthermore report on the SSMT solver SiSAT including recent enhancements in terms of solver performance, expressiveness of the input language, and handling of numerical issues. The significance of the performance enhancements is demonstrated by empirical results.

Keywords: Probabilistic hybrid systems, probabilistic logic, constraint satisfaction problems, problem solvers, automatic verification
Subproject(s): H1/2,H4

Abstract (click to open/close)

Dynamic Evolution Systems describe an emerging class of systems that vary dynamically in size and topology. Typical examples include the adhoc networking principle where a routing infrastructure over a changing set of participants is created and maintained. A corresponding routing protocol has to be able to handle an arbitrary number of nodes and must in particular be prepared for the integration of new and the proper dismissal of disappeared devices. Similar structures occur in dynamic traffic management systems like the car platooning scenario where physically adjacent cars establish interlinked groups. This thesis presents a formal method to check whether a system in the sense above adheres to requirements given in form of temporal scenarios. We observe that the inherent unboundedness of the systems renders this task in general undecidable and we present a sound but necessarily incomplete solution that is based on the abstract-check-refine paradigm. Our approach employs the spotlight abstraction principle to obtain a finite description of both the system and the requirement. The idea of this abstraction technique is to exactly preserve the behaviour of a finite set of spotlight processes and to provide one dedicated abstract process to over-approximate the behaviour of the non-spotlight processes. As the validity of a requirement often cannot be definitely decided in the initial abstraction, we propose an automatic and iterative refinement of the abstraction that is guided by the analysis of abstract counterexamples. The refinement method is based on the observation that the precision of the abstraction can be tuned by two complementary principles, namely by enlarging the size of the spotlight and by refining the behaviour of the non-spotlight part of the abstraction. We demonstrate that the approach can be further improved by integrating auxiliary system invariants, and we devise a static analysis method to obtain such invariants for an existing modelling language. Our approach is realised in form of a tool implementation. On this basis, we perform a practical evaluation of our approach on a number of case studies that cover a broad range of the addressed class of systems. We are in particular able to automatically establish system properties for which manual intervention was required before.

Subproject(s): S2

Abstract (click to open/close)

How can analyses for probabilistic systems be achieved that are optimal, in the sense that they enjoy the best possible precision for a given abstraction? Aiming at the problem at the heart of many algorithms for probabilistic model checking -- computing the probability of reaching a particular set of states -- we leverage the theory of abstract interpretation, obtaining, for the first time, a characterization of such optimal analyses in this setting. With a focus on concurrent system and predicate abstraction, the paper gives ways to efficiently compute, approximate and refine such abstractions, and an experimental evaluation.

Subproject(s): S2

Abstract (click to open/close)

Directed model checking is a well-established technique to tackle the state explosion problem when the aim is to find error states in large systems. In this approach, the state space traversal is guided through a function that estimates the distance to nearest error states. States with lower estimates are preferably expanded during the search. Obviously, the challenge is to develop distance functions that are efficiently computable on the one hand and as informative as possible on the other hand. In this paper, we introduce the causal graph structure to the context of directed model checking. Based on causal graph analysis, we first adapt a distance estimation function from AI planning to directed model checking. Furthermore, we investigate an abstraction that is guaranteed to preserve error states. The experimental evaluation shows the practical potential of these techniques.

Subproject(s): R3

Abstract (click to open/close)

Directed model checking is a well-established technique that is tailored to fast detection of system states that violate a given safety property. This is achieved by influencing the order in which states are explored during the state space traversal. The order is typically determined by an abstract distance function that estimates a state's distance to a nearest error state. In this paper, we propose a general enhancement to directed model checking based on the evaluation of state transitions. We present a schema, parametrized by an abstract distance function, to evaluate transitions and propose a new method for the state space traversal. Our framework can be applied automatically to a wide range of abstract distance functions. The empirical evaluation impressively shows its practical potential. Apparently, the new method identifies a sweet spot in the trade-off between scalability (memory consumption) and short error traces.

Subproject(s): R3

Abstract (click to open/close)

The goal of program verification is to ensure software reliability by establishing a mathematical proof which guarantees that the software behaves correctly. Program analysis tools assist the developer in the verification process. Ideally a program analysis should be applicable to a wide range of verification problems without imposing a high burden on its users, i.e., without requiring deep mathematical knowledge and experience in program verification. A big step forward towards this ideal has been achieved by combining "abstract interpretation" with techniques for "automated reasoning". In abstract interpretation one transforms the "concrete program" into an "abstract program". The abstract program enables the analysis to statically collect information over all possible executions of the concrete program. This information is used to automatically verify the correctness of the concrete program. Abstract interpretation increases the degree of automation in verification by shifting the burden of formally reasoning about programs from the developer to the designer of the program analysis. Automated reasoning pushes the degree of automation even further. It enables the automatic construction of the abstraction for a specific program and a specific correctness property and (if necessary) the automatic refinement of this abstraction. We refer to program analyses that combine abstract interpretation with automated reasoning as "symbolic program analysis". A problem that has recently seen much attention in program verification is the question of how to effectively deal with linked heap-allocated data structures. Program analyses that target properties of these data structures are commonly referred to as "shape analyses". A symbolic shape analysis promises to handle a spectrum of different linked heap-allocated data structures, and a spectrum of properties to verify, without requiring the user to manually adjust the analysis to the specific problem instance. It was open what a symbolic shape analysis would look like. In this thesis we are concerned with this question. We present "domain predicate abstraction", which generalizes predicate abstraction to the point where it becomes effectively applicable for shape analysis. Domain predicate abstraction incorporates the key idea of three-valued shape analysis into predicate abstraction by replacing predicates on program states by predicates on objects in the heap of program states. We show how to automate the transformation of a heap-manipulating program into an abstract program using automated reasoning procedures. We further develop an abstraction refinement technique that complements domain predicate abstraction to a fully automated symbolic shape analysis. Finally, we present "field constraint analysis", a new technique for reasoning about heap programs. Field constraint analysis enables the application of decision procedures for reasoning about specific data structures (such as trees) to arbitrary data structures. This technique makes our symbolic shape analysis applicable to the diverse data structures that occur in practice. All the techniques presented in this thesis have been implemented and evaluated in the Bohne Verifier. We used Bohne to verify complex user-specified properties of data structure implementations. For instance, we were able to verify preservation of data structure invariants for operations on threaded binary trees (including sortedness and the in-order traversal invariant) without manually adjusting the analysis to this specific problem or providing user assistance beyond stating the properties to verify. We are not aware of any other shape analysis that can verify such properties with a comparable degree of automation.

Subproject(s): S2

Abstract (click to open/close)

Static worst-case execution time analysis of real-time tasks is based on abstract models that capture the timing behavior of the processor on which the tasks run. For complex processors, task-level execution time bounds are obtained by a state exploration which involves the abstract model and the program. Partial state space exploration is not sound. A full exploration can become too expensive. We present a novel symbolic method for WCET analysis based on abstract pipeline models which produces sound results and is scalable in terms of the considered hardware states.

Subproject(s): R2

Abstract (click to open/close)

Embedded hard real-time systems need reliable guarantees for the satisfaction of their timing constraints. Experience with the use of static timing analysis methods and the tools based on them in the automotive and the aeronautics industries is positive. However, both the precision of the results and the efficiency of the analysis methods are highly dependent on the predictability of the execution platform. In fact, the architecture determines whether a static timing analysis is practically feasible at all and whether the most precise obtainable results are precise enough. Results contained in the paper also show that measurement-based methods still used in industry are not useful for quite commonly used complex processors. This dependence on the architectural development is of growing concern to the developers of timing analysis tools and their customers, the developers in industry. The problem reaches a new level of severity with the advent of multi-core architectures in the embedded domain. This article describes the architectural influence on static timing analysis and gives recommendations as to profitable and unacceptable architectural features.

Subproject(s): R2

Abstract (click to open/close)

Since its introduction in 1999, bounded model checking has gained industrial relevance for detecting errors in digital and hybrid systems. One of the main reasons for this is that it always provides a counterexample when an erroneous execution trace is found. Such a counterexample can guide the designer while debugging the system.

In this paper we are investigating how bounded model checking can be applied to generate counterexamples for a different kind of model--namely discrete-time Markov chains. Since in this case counterexamples in general do not consist of a single path to a safety-critical state, but of a potentially large set of paths, novel optimization techniques like loop-detection are applied not only to speed-up the counterexample computation, but also to reduce the size of the counterexamples significantly. We report on some experiments which demonstrate the practical applicability of our method.

Subproject(s): S3

Abstract (click to open/close)

Hard real-time systems induce strict constraints on the timing of the task set. Validation of these timing constraints is thus a major challenge during the design of such a system. Whereas the derivation of timing guarantees must already be considered complex if tasks are running to completion, it gets even more complex if tasks are scheduled preemptively - especially due to caches, deployed to improve the average performance. In this paper we propose new method to compute valid upper bounds on a task's worst case execution time (WCET). Our method approximates an optimal memory layout such that the set of possibly evicted cache-entries during preemption is minimized. This set then delivers information to bound the execution time of tasks under preemption in an adopted WCET analysis.

Subproject(s): R2

Abstract (click to open/close)

Hard real-time systems have stringent timing constraints expressed in units of time. To ensure that a task finishes within its time-frame, the designer of such a system must be able to derive upper bounds on the task's worst case execution time (WCET). To compute such upper bounds, timing analyses are used. These analyses require that information such as bounds on the maximum numbers of loop iterations are known statically, i.e. during design time. Parametric timing analysis softens these requirements: it yields symbolic formulas instead of single numeric values representing the upper bound on the task's execution time. In this paper, we present a new parametric timing analysis that is able to derive safe and precise results. Our method determines what the parameters of the program are, constructs parametric loop bounds, takes processor behaviour into account and attains a formula automatically. In the end, we present tests to show that the precision and runtime of our analysis are very close to those of numeric timing analysis.

Subproject(s): R2

Abstract (click to open/close)

Bounded model checking of partial circuit designs enables the detection of errors even when the implementation of the design is not finished. The behavior of the missing parts can be modeled by a conservative extension of propositional logic, called 01X-logic. Then the transitions of the underlying (incomplete) sequential circuit under verification have to be represented adequately. In this work, we investigate the difference between a relation-oriented and a function-oriented approach for this issue. Experimental results on a large set of examples show that the function-oriented representation is most often superior w. r. t. (1) CPU runtime and (2) accuracy regarding the ability to find a counterexample, such that by using the function-oriented approach an increase of accuracy up to 210% and a speed-up of the CPU runtime up to 390% compared to the relation-oriented approach are achieved. But there are also relevant examples, e. g. a VLIW-ALU, for which the relation-oriented approach outperforms the function-oriented one by 300% in terms of CPU-time, showing that both approaches are efficient for different scenarios.

Subproject(s): S1

Abstract (click to open/close)

In contrast to classical planning, in adversarial planning, the planning agent has to face an adversary trying to prevent him from reaching his goals. In this paper, we investigate a forward-chaining approach to adversarial planning based on the AO* algorithm. The exploration of the underlying AND/OR graph is guided by a heuristic evaluation function, inspired by the relaxed planning graph heuristic used in the FF planner. Unlike FF, our heuristic uses an adversarial planning graph with distinct proposition and action layers for the protagonist and antagonist. First results suggest that in certain planning domains, our approach yields results competitive with the state of the art.

Subproject(s): S1

Abstract (click to open/close)

In this report we show how fault injection together with recent advances in stochastic model checking can be combined to form a crucial ingredient for improving quantitative safety analysis. Based on standard design notations (Statecharts) annotated with fault occurrence distributions we compute the probability of reaching a safety-critical state and to what extent certain fault configurations contribute to this probability.

Subproject(s): S3

Abstract (click to open/close)

We show how fault injection together with recent advances in stochastic model checking can be combined to form a crucial ingredient for improving quantitative safety analysis. Based on standard design notations (Statecharts) annotated with fault occurrence distributions we compute to what extent certain fault con?gurations contribute to the probability of reaching a safety-critical state.

Subproject(s): S3

Abstract (click to open/close)

Abstraction and slicing are both techniques for reducing the size of the state space to be inspected during verification. In this paper, we present a new model checking procedure for infinite-state concurrent systems that interleaves automatic abstraction refinement, which splits states according to new predicates obtained by Craig interpolation, with slicing, which removes irrelevant states and transitions from the abstraction. The effects of abstraction and slicing complement each other. As the refinement progresses, the increasing accuracy of the abstract model allows for a more precise slice; the resulting smaller representation gives room for additional predicates in the abstraction. The procedure terminates when an error path in the abstraction can be concretized, which proves that the system is erroneous, or when the slice becomes empty, which proves that the system is correct.

Subproject(s): R1

Abstract (click to open/close)

This paper presents a novel algorithm to compute weak bisimulation quotients for finite acyclic models. It is developed in the setting of interactive Markov chains, a model overarching both labelled transition systems and continuous-time Markov chains. This model has lately been used to give an acyclic compositional semantics to dynamic fault trees, a reliability modelling formalism. While the theoretical complexity does not change substantially, the algorithm performs very well in practice, almost linear in the size of the input model. We use a number of case studies to show that it is vastly more efficient than the standard bisimulation minimisation algorithms. In particular we show the effectiveness in the analysis of dynamic fault trees.

Subproject(s): S3

Abstract (click to open/close)

Counterexample-guided abstraction refinement (CEGAR) is used in automated software analysis to find suitable finite-state abstractions of infinite-state systems. In this paper, we extend CEGAR to games with incomplete information, as they commonly occur in controller synthesis and modular verification. The challenge is that, under incomplete information, one must carefully account for the knowledge available to the player: the strategy must not depend on information the player cannot see. We propose an abstraction mechanism for games under incomplete information that incorporates the approximation of the players' moves into a knowledge-based subset construction on the abstract state space. This abstraction results in a perfect-information game over a finite graph. The concretizability of abstract strategies can be encoded as the satisfiability of strategy-tree formulas. Based on this encoding, we present an interpolation-based approach for selecting new predicates and provide sufficient conditions for the termination of the resulting refinement loop.

Subproject(s): S1

Abstract (click to open/close)

Counterexample-guided abstraction refinement (CEGAR) is used in automated software analysis to find suitable finite-state abstractions of infinite-state systems. In this paper, we extend CEGAR to games with incomplete information, as they commonly occur in controller synthesis and modular verification. The challenge is that, under incomplete information, one must carefully account for the knowledge available to the player: the strategy must not depend on information the player cannot see. We propose an abstraction mechanism for games under incomplete information that incorporates the approximation of the players' moves into a knowledge-based subset construction on the abstract state space. This abstraction results in a perfect-information game over a finite graph. The concretizability of abstract strategies can be encoded as the satisfiability of strategy-tree formulas. Based on this encoding, we present an interpolation-based approach for selecting new predicates and provide sufficient conditions for the termination of the resulting refinement loop.

Subproject(s): S1

Abstract (click to open/close)

Lazy abstraction builds up an abstract reachability tree by locally refining abstractions in order to eliminate spurious counterexamples in smaller and smaller subtrees. The method has proven useful to verify systems code. It is still open how good the method is as a decision procedure, i.e., whether the method terminates for already known decidable verification problems. In this paper, we answer the question positively for broadcast protocols and other infinite-state models in the class of so-called well-structured systems. This extends an existing result on systems with a finite bisimulation quotient.

Subproject(s): R1

Abstract (click to open/close)

We introduce subsequence invariants, which characterize the behavior of a concurrent system in terms of the occurrences of synchronization events. Unlike state invariants, which refer to the state variables of the system, subsequence invariants are defined over auxiliary counter variables that reflect how often the event sequences from a given set have occurred so far. A subsequence invariant is a linear constraint over the possible counter values. We allow every occurrence of a subsequence to be interleaved arbitrarily with other events. As a result, subsequence invariants are preserved when a given process is composed with additional processes. Subsequence invariants can therefore be computed individually for each process and then be used to reason about the full system. We present an efficient algorithm for the synthesis of subsequence invariants. Our construction can be applied incrementally to obtain a growing set of invariants given a growing set of event sequences.

Subproject(s): S1

Abstract (click to open/close)

We introduce subsequence invariants, which characterize the behavior of a concurrent system in terms of the occurrences of synchronization events. Unlike state invariants, which refer to the state variables of the system, subsequence invariants are defined over auxiliary counter variables that reflect how often the event sequences from a given set have occurred so far. A subsequence invariant is a linear constraint over the possible counter values. We allow every occurrence of a subsequence to be interleaved arbitrarily with other events. As a result, subsequence invariants are preserved when a given process is composed with additional processes. Subsequence invariants can therefore be computed individually for each process and then be used to reason about the full system. We present an efficient algorithm for the synthesis of subsequence invariants. Our construction can be applied incrementally to obtain a growing set of invariants given a growing set of event sequences.

Subproject(s): R1,R3

Abstract (click to open/close)

In the analysis of hybrid discrete-continuous systems, rich arithmetic constraint formulae with complex Boolean structure arise naturally. The iSAT algorithm, a solver for such formulae, is aimed at bounded model checking of hybrid systems. In this paper, we identify challenges emerging from planned and ongoing work to enhance the iSAT algorithm: First, we propose an extension of iSAT to directly handle ordinary differential equations as constraints. Second, we outline the recently introduced generalization of the iSAT algorithm to deal with probabilistic hybrid systems and some open research issues in that context. Third, we present ideas on how to move from bounded to unbounded model checking by using the concept of interpolation. Finally, we discuss the adaption of some parallelization techniques to the iSAT case, which will hopefully lead to performance gains in the future. By presenting these open research questions, this paper aims at fostering discussions on these extensions of constraint solving.

Subproject(s): H1/2,H4

Abstract (click to open/close)

In order to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving ordinary differential equations (ODEs), we provide a seamless integration of safe numeric overapproximation of initial-value problems into a SAT-modulo-theory (SMT) approach to interval-based arithmetic constraint solving. Interval-based safe numeric approximation of ODEs is used as an interval contractor being able to narrow candidate sets in phase space in both temporal directions: post-images of ODEs (i.e., sets of states reachable from a set of initial values) are narrowed based on partial information about the initial values and, vice versa, pre-images are narrowed based on partial knowledge about post-sets. In contrast to the related CLP(F) approach of Hickey and Wittenberg, we do (a) support coordinate transformations mitigating the wrapping effect encountered upon iterating interval-based overapproximations of reachable state sets and (b) embed the approach into an SMT framework, thus accelerating the solving process through the algorithmic enhacements of recent SAT solving technology.

Subproject(s): H1/2

Abstract (click to open/close)

In order to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving ordinary differential equations (ODEs), we provide a seamless integration of safe numeric overapproximation of initial-value problems into a SAT-modulo-theory (SMT) approach to interval-based arithmetic constraint solving. Interval-based safe numeric approximation of ODEs is used as an interval contractor being able to narrow candidate sets in phase space in both temporal directions: post-images of ODEs (i.e., sets of states reachable from a set of initial values) are narrowed based on partial information about the initial values and, vice versa, pre-images are narrowed based on partial knowledge about post-sets. In contrast to the related CLP(F) approach of Hickey and Wittenberg, we do (a) support coordinate transformations mitigating the wrapping effect encountered upon iterating interval-based overapproximations of reachable state sets and (b) embed the approach into an SMT framework, thus accelerating the solving process through the algorithmic enhancements of recent SAT solving technology.

Subproject(s): H1/2

Abstract (click to open/close)

Automata-based decision procedures have proved to be a particularly useful tool for infinite-state model checking, where automata are used to represent sets of real and integer values. However, not all theoretical aspects of these decision procedures are completely understood. We establish triple exponential upper bounds on the automata size for FO(Z,+,<) and FO(R,Z,+,<). While a similar bound for Presburger Arithmetic, i.e., FO(Z,+,<) was obtained earlier using a quantifier elimination based approach, the bound for FO(R,Z,+,<) is novel. We define two graded back-and-forth systems, and use them to derive bounds on the automata size by establishing a connection between those systems and languages that can be described by formulas in the respective logics. With these upper bounds that match the known lower bounds, the theoretical background for automata-based decision procedures for linear arithmetics becomes more complete.

Subproject(s): H1/2

Abstract (click to open/close)

Automata have proved to be a useful tool in infinite-state model checking, since they can represent infinite sets of integers and reals. However, analogous to the use of binary decision diagrams (BDDs) to represent finite sets, the sizes of the automata are an obstacle in the automata-based set representation. In this article, we generalize the notion of “don’t cares� for BDDs to word languages as a means to reduce the automata sizes. We show that the minimal weak deterministic Büchi automaton (WDBA) with respect to a given don’t care set, under certain restrictions, is uniquely determined and can be efficiently constructed. We apply don’t cares to improve the efficiency of a decision procedure for the first-order logic over the mixed linear arithmetic over the integers and the reals based on WDBAs.

Subproject(s): H1/2

Abstract (click to open/close)

The requirement synthesis tool RESY automatically computes environment assumptions for compositional model checking. Given a process M in a multi-process PROMELA program, an abstraction refinement loop computes a coarse equivalence relation on the states of the environment, collapsing two states if the environment of M can either force the occurrence of an error from both states or from neither state. RESY supports three different operation modes: assumption generation, compositional model checking, and front-end to the model checker SPIN. In assumption generation mode, RESY minimizes the size of the assumption; small assumptions are useful for program documentation and as certificates for re-verification. In compositional model checking mode, RESY terminates as soon as the property is proven or disproven, independently of the size of the assumption. In front-end mode, RESY terminates when the size of the assumption falls below a specified threshold, and calls SPIN with the simplified verification problem.

Subproject(s): S1

Abstract (click to open/close)

We present an automatic method for the synthesis of certificates for components in embedded real-time systems. A certificate is a small homomorphic abstraction that can transparently replace the component during model checking: if the verification with the certificate succeeds, then the component is guaranteed to be correct; if the verification with the certificate fails, then the component itself must be erroneous. We give a direct construction, based on a forward and backward reachability analysis of the timed system, and an iterative refinement pocess, which produces a series of successively smaller certificates. In our experiments, model checking the certificate is several orders of magnitude faster than model checking the original system.

Subproject(s): S1

Subproject(s): H1/2,H4

Abstract (click to open/close)

Duration Calculus (abbreviated to DC) is an intervalbased, metric-time temporal logic designed for reasoning about embedded real-time systems at a high level of abstraction. But the complexity of model checking any decidable fragment featuring both negation and chop, DC's only modality, is non-elementary and thus impractical. We here investigate a similar approximation as frequently employed in model checking situation-based temporal logics, where linear-time problems are safely approximated by branching-time counterparts amenable to more efficient model-checking algorithms. Mimicking the role that a situation has in (A)CTL as origin of a set of linear traces, we define a branching-time counterpart to intervalbased temporal logics building on situation pairs spanning sets of intervals. While this branching-time interval semantics yields the desired reduction in complexity of the modelchecking problem, from non-elementary to linear in the size of the formula and cubic in the size of the model, the approximation is too coarse to be practical. We therefore refine the semantics by an occurrence count for crucial states (e.g., cuts of loops) in the model, arriving at a 4-fold exponential model-checking problem sufficiently accurately approximating the original one.

Subproject(s): R1

Abstract (click to open/close)

The analysis of hybrid systems exhibiting probabilistic behaviour is notoriously difficult. To enable mechanised analysis of such systems, we extend the reasoning power of arithmetic satisfiability-modulotheory solving (SMT) by a comprehensive treatment of randomized (a.k.a. stochastic) quantification over discrete variables within the mixed Booleanarithmetic constraint system. This provides the technological basis for a fully symbolic analysis of probabilistic hybrid automata. Generalizing SMT-based bounded model-checking of hybrid automata [2, 11], stochastic SMT permits the direct and fully symbolic analysis of probabilistic bounded reachability problems of probabilistic hybrid automata without resorting to approximation by intermediate finite-state abstractions.

Subproject(s): H1/2,H4

Abstract (click to open/close)

The analysis of hybrid systems exhibiting probabilistic behaviour is notoriously difficult. To enable mechanised analysis of such systems, we extend the reasoning power of arithmetic satisfiability-modulo-theory solving (SMT) by a comprehensive treatment of randomized (a.k.a. stochastic) quantification over discrete variables within the mixed Boolean-arithmetic constraint system. This provides the technological basis for a fully symbolic analysis of probabilistic hybrid automata. Generalizing SMT-based bounded model-checking of hybrid automata [2,9], stochastic SMT permits the direct and fully symbolic analysis of probabilistic bounded reachability problems of probabilistic hybrid automata without resorting to approximation by intermediate finite-state abstractions.

Keywords: Stochastic satisfiability, infinite domains, probabilistic hybrid automata, probabilistic bounded reachability.
Subproject(s): H1/2,H4

Abstract (click to open/close)

Caches are commonly employed to hide the latency gap between memory and the CPU by exploiting locality in memory accesses. The cache performance strongly influences a system's overall performance, as this gap is large and ever-increasing. The efficiency of a given cache architecture -- usually measured by its miss ratio -- varies greatly depending on the software being executed. We present an efficient method to estimate the miss ratio using a stochastic model. The model takes into account the parameters of the cache architecture and a concise characterization of the software's locality. In contrast to previous approaches, we consider the replacement policy as an important component of the cache architecture. To this end, we introduce policy tables as a concise representation of replacement policies. The software's locality is characterized by stack histograms or our extension thereof: History stack histograms, which refine stack histograms by distinguishing contexts of accesses. Simulation results on the SPEC benchmarks demonstrate the strong influence of the replacement policy on the miss ratio and the precision of our estimates: average absolute errors between 0,18% and 2,92%.

Subproject(s): R2

Subproject(s): S1

Abstract (click to open/close)

Many current heuristics for domain-independent planning, such as Bonet and Geffner's additive heuristic and Hoffmann and Nebel's FF heuristic, are based on delete relaxations. They estimate the goal distance of a search state by approximating the solution cost in a relaxed task where negative consequences of operator applications are ignored. Helmert's causal graph heuristic, on the other hand, approximates goal distances by solving a hierarchy of "local" planning problems that only involve a single state variable and the variables it depends on directly. Superficially, the causal graph heuristic appears quite unrelated to heuristics based on delete relaxation. In this contribution, we show that the opposite is true. Using a novel, declarative formulation of the causal graph heuristic, we show that the causal graph heuristic is the additive heuristic plus context. Unlike the original heuristic, our formulation does not require the causal graph to be acyclic, and thus leads to a proper generalization of both the causal graph and additive heuristics. Empirical results show that the new heuristic is significantly better informed than both Helmert's original causal graph heuristic and the additive heuristic and outperforms them across a wide range of standard benchmarks.

Subproject(s): S1

Abstract (click to open/close)

The efficiency of optimal planning algorithms based on heuristic search crucially depends on the accuracy of the heuristic function used to guide the search. Often, we are interested in domain-independent heuristics for planning. In order to assess the limitations of domain-independent heuristic planning, it appears interesting to analyse the (in)accuracy of common domain-independent planning heuristics in the IPC benchmark domains. For a selection of these domains, we analytically investigate the accuracy of the h+ heuristic, the hm family of heuristics, and certain (additive) pattern database heuristics, compared to the perfect heuristic h*. Whereas h+ and additive pattern database heuristics usually return cost estimates proportional to the true cost, non-additive hm and non-additive pattern-database heuristics can yield results underestimating the true cost by arbitrarily large factors.

Subproject(s): S1

Abstract (click to open/close)

Heuristic search using algorithms such as A* and IDA* is the prevalent method for obtaining optimal sequential solutions for classical planning tasks. Theoretical analyses of these classical search algorithms, such as the well-known results of Pohl, Gaschnig and Pearl, suggest that such heuristic search algorithms can obtain better than exponential scaling behaviour, provided that the heuristics are accurate enough. Here, we show that for a number of common planning benchmark domains, including ones that admit optimal solution in polynomial time, general search algorithms such as A* must necessarily explore an exponential number of search nodes even under the optimistic assumption of almost perfect heuristic estimators, whose heuristic error is bounded by a small additive constant. Our results shed some light on the comparatively bad performance of optimal heuristic search approaches in "simple" domains such as GRIPPER. They suggest that in many domains, further improvements in run-time require changes to other parts of the planning algorithm than the heuristic estimator.

Subproject(s): S1,R3

Abstract (click to open/close)

Many AI problems can be recast as finding an optimal path in a discrete state space. An abstraction defines an admissible heuristic function as the distances in a smaller state space where arbitrary sets of states are "aggregated" into single states. A special case are pattern database (PDB) heuristics, which aggregate states iff they agree on the state variables inside the pattern. Explicit-state abstraction is more flexible, explicitly aggregating selected pairs of states in a process that interleaves composition of abstractions with abstraction of the composites. The increased flexibility gains expressive power: sometimes, the real cost function can be represented concisely as an explicit-state abstraction, but not as a PDB. Explicit-state abstraction has been applied to planning and model checking, with highly promising empirical results.

Subproject(s): S1

Abstract (click to open/close)

In this paper we describe the complete workflow of analyzing the dynamic behavior of safety-critical embedded systems with HySAT. HySAT is an arithmetic constraint solver with a tightly integrated bounded model checker for hybrid discrete-continuous systems which - in contrast to many other solvers - is not confined to linear arithmetic, but can also deal with nonlinear constraints involving transcendental functions. Based on a controller for train separation implementing a "moving block" interlocking scheme in the forthcoming European Train Control System Level 3, we exemplify the usage of the tool over the whole cycle from encoding a hybrid system to interpreting the results.

Subproject(s): H1/2

Abstract (click to open/close)

Counterexample-guided abstraction refinement (CEGAR) has been en vogue for the automatic verification of very large systems in the past years. When trying to apply CEGAR to the verification of probabilistic systems, various foundational questions arise. This paper explores them in the context of predicate abstraction.

Subproject(s): S2, S3

Abstract (click to open/close)

Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a perfect term-generated model for the theory. Proving universal properties with respect to a saturated theory directly leads to a modification of the perfect model's term-generated domain, as new Skolem functions are introduced. For many applications, this is not desired. Therefore, we propose the first superposition calculus that can explicitly represent existentially quantified variables and can thus compute with respect to a given domain. This calculus is sound and complete for a first-order fixed domain semantics. For some classes of formulas and theories, we can even employ the calculus to prove properties of the perfect model itself, going beyond the scope of known superposition based approaches.

Subproject(s): H1/2

Abstract (click to open/close)

We present a general framework which allows to identify complex theories important in verification for which efficient reasoning methods exist. The framework we present is based on a general notion of locality. We show that locality considerations allow us to obtain parameterized decidability and complexity results for many (combinations of) theories important in verification in general and in the verification of parametric systems in particular. We give numerous examples; in particular we show that several theories of data structures studied in the verification literature are local extensions of a base theory. The general framework we use allows us to identify situations in which some of the syntactical restrictions imposed in previous papers can be relaxed.

Subproject(s): R1

Abstract (click to open/close)

Local reasoning allows to handle SMT problems involving a certain class of universally quantified formulas in a complete way by instantiation to a finite set of ground formulas. We present a method to generate this set incrementally, in order to provide a more efficient way of solving these satisfiability problems. The incremental instantiation is guided semantically, inspired by the instance generation approach to first-order theorem proving. Our method is sound and complete, and terminates on both satisfiable and unsatisfiable input after generating a subset of the instances needed in standard local reasoning.

Subproject(s): R1

Abstract (click to open/close)

Directed model checking aims at speeding up the search for bugs in a system through the use of heuristic functions. Such a function maps states to integers, estimating the state's distance to the nearest error state. The search gives a preference to states with lower estimates. The key issue is how to generate good heuristic functions, i.e., functions that guide the search quickly to an error state. An arsenal of heuristic functions has been developed in recent years. Significant progress was made, but many problems still prove to be notoriously hard. In particular, a body of work describes heuristic functions for model checking timed automata in Uppaal, and tested them on a certain set of benchmarks. Into this arsenal we add another heuristic function. With previous heuristics, for the largest of the benchmarks it was only just possible to find some (unnecessarily long) error path. With the new heuristic, we can find provably shortest error paths for these benchmarks in a matter of seconds. The heuristic function is based on a kind of Russian Doll principle, where the heuristic for a given problem arises through using Uppaal itself for the complete exploration of a simplified instance of the same problem. The simplification consists in removing those parts from the problem that are distant from the error property. As our empirical results confirm, this simplification often preserves the characteristic structure leading to the error.

Subproject(s): R3

Abstract (click to open/close)

It is probably very hard to develop a new model checker that is faster than textsc Uppaal for verifying (correct) timed automata. In fact, our tool textsc Mcta does not even try to compete with textsc Uppaal in this (i. e., textsc Uppaal's) arena. Instead, textsc Mcta is geared towards analyzing incorrect specifications of timed automata. It returns (shorter) error traces faster.

Subproject(s): R3

Abstract (click to open/close)

In recent years, the use of constraint solvers for analysis and verification of industrial systems has become increasingly popular. The correctness and reliability of the results returned by the employed solvers are a vital requirement, in particular for safety-critical systems. If a solver proves the satisfiability of a constraint system and returns a solution then the answer of the solver can be validated by means of the solution. However, in case the solver claims that the constraint system is unsatisfiable without any certificate then the validation of this answer is not that simple. In this paper, we establish the theoretical basis of generating proofs of unsatisfiability in the mixed Boolean and non-linear arithmetic constraint framework over the reals and integers. To do so, we propose a simple rule-based calculus for unsatisfiable mixed Boolean-arithmetic constraints to produce and check unsatisfiability proofs. Furthermore, we enhance the iSAT constraint solver to generate unsatisfiability proofs, we implement a tool validating such proofs, and give some experimental results.

Subproject(s): H1/2

Abstract (click to open/close)

Scheduling analysis for simplified distributed real-time systems, where the worst case execution time (WCET) of each task is fixed, is well understood. However, often the simplified assumption of fixed WCETs lacks accuracy, e.g. it may have a high variance depending on internal task states. Even if the transition relation of task's internal states is known, traditionally applied scalable analysis approaches cannot exploit this information in order to yield more accurate response times. In this paper we propose a new type of analysis for this kind of real-time systems. Our approach is based on a transformation of response time analysis into a satisfiability problem, enriched by task internal automata. Evaluations show the powerfulness of this analysis and, furthermore, we will exemplify how our approach can be used to analyse systems with mixed temporal and functional characterisations.

Subproject(s): R2

Abstract (click to open/close)

Model checking of real-time systems against Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to realistic applications. Our algorithm significantly extends the subset of DC that can be checked automatically. The central part of the algorithm is the automatic decomposition of DC specifications into sub-properties that can be verified independently. The decomposition is based on a novel distributive law for DC. We implemented the algorithm in a tool chain for the automated verification of systems comprising data, communication, and real-time aspects. We applied the tool chain to verify safety properties in an industrial case study from the European Train Control System (ETCS).

Keywords: Model checking, Verification, Duration Calculus, Timed automata, Real-time systems, European Train Control System, Case study
Subproject(s): R1

Abstract (click to open/close)

Fault tolerance measures can be used to distinguish between different self-stabilizing solutions to the same problem. However, derivation of these measures via analysis suffers from limitations with respect to scalability of and applicability to a wide class of self-stabilizing distributed algorithms. We describe a simulation framework to derive fault tolerance measures for self-stabilizing algorithms which can deal with the complete class of self-stabilizing al- gorithms. We show the advantages of the simulation framework in contrast to the analytical approach not only by means of accuracy of results, range of applicable scenarios and performance, but also for investigation of the influence of schedulers on a meta level and the possibility to simulate large scale systems featuring dynamic fault probabilities.

Subproject(s): H4

Abstract (click to open/close)

We generalise dynamic logic to a logic for differential-algebraic programs, i.e., discrete programs augmented with first-order differential-algebraic formulas as continuous evolution constraints in addition to first-order discrete jump formulas. These programs characterise interacting discrete and continuous dynamics of hybrid systems elegantly and uniformly. For our logic, we introduce a calculus over real arithmetic with discrete induction and a new differential induction with which differential-algebraic programs can be verified by exploiting their differential constraints algebraically without having to solve them. We develop the theory of differential induction and differential refinement and analyse their deductive power. As a case study, we present parametric tangential roundabout maneuvers in air traffic control and prove collision avoidance in our calculus.

Keywords: dynamic logic, differential constraints, sequent calculus, verification of hybrid systems, differential induction, theorem proving
Subproject(s): H3

Abstract (click to open/close)

Hybrid systems are models for complex physical systems and are defined as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. With the goal of developing a theoretical and practical foundation for deductive verification of hybrid systems, we introduce a dynamic logic for hybrid programs, which is a program notation for hybrid systems. As a verification technique that is suitable for automation, we introduce a free variable proof calculus with a novel combination of real-valued free variables and Skolemisation for lifting quantifier elimination for real arithmetic to dynamic logic. The calculus is compositional, i.e., it reduces properties of hybrid programs to properties of their parts. Our main result proves that this calculus axiomatises the transition behaviour of hybrid systems completely relative to differential equations. In a case study with cooperating traffic agents of the European Train Control System, we further show that our calculus is well-suited for verifying realistic hybrid systems with parametric system dynamics.

Keywords: dynamic logic, differential equations, sequent calculus, axiomatisation, automated theorem proving, verification of hybrid systems
Subproject(s): H3

Abstract (click to open/close)

We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose right-hand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control.

Keywords: verification of hybrid systems, differential invariants, verification logic, fixedpoint engine
Subproject(s): H3

Abstract (click to open/close)

KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic, which is a real-valued first-order dynamic logic for hybrid programs, a program notation for hybrid automata. For automating the verification process, KeYmaera implements a generalized free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically. To overcome the complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy. Our tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying collision avoidance in case studies from train control and air traffic management.

Keywords: dynamic logic, automated theorem proving, decision procedures, computer algebra, verification of hybrid systems
Subproject(s): H3

Abstract (click to open/close)

We formally verify hybrid safety properties of cooperation protocols in a fully parametric version of the European Train Control System (ETCS). We present a formal model using hybrid programs and verify correctness using our logic-based decomposition procedure. This procedure supports free parameters and parameter discovery, which is required to determine correct design choices for free parameters of ETCS.

Keywords: parametric verification, logic for hybrid systems, symbolic decomposition
Subproject(s): H3

Subproject(s): S2