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)

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 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)

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)

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)

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)

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)

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)

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

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

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)

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)

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)

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 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)

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)

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)

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

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

Abstract (click to open/close)

Acyclic phase-type distributions are phase-type distributions with triangular matrix representations. They constitute a versatile modelling tool, since they (1) can serve as approximations to any continuous distributions, and (2) exhibit special properties and characteristics, which usually result in some ease in analysis. The size of the 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 report proposes an effective procedure to aggregate the size of the matrix representation without altering the distribution.

Subproject(s): S3

Subproject(s): H1/2

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. On today's architectures a cache miss may cost several hundred CPU cycles. In order to fulfill stringent performance requirements, caches are now also used in hard real-time systems. In such systems, upper and sometimes also lower bounds on the execution times of a task have to be computed. To obtain tight bounds, timing analyses must take into account the cache architecture. However, developing cache analyses -- analyses that determine whether a memory access is a hit or a miss -- is a difficult problem for some cache architectures. In this paper, we present a tool to automatically compute relative competitive ratios for a large class of replacement policies, including LRU, FIFO, and PLRU. Relative competitive ratios bound the performance of one policy relative to the performance of another policy. These performance relations allow us to use cache-performance predictions for one policy to compute predictions for another, including policies that could previously not be dealt with.

Subproject(s): R2

Subproject(s): R2

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. On today's architectures a cache miss may cost several hundred CPU cycles. In order to fulfill stringent performance requirements, caches are also used in hard real-time systems. In such systems, upper and lower bounds on the execution time of tasks have to be computed. Different methods have been proposed for timing analysis, including measurement and static analysis. The sensitivity of a cache replacement policy expresses to what extent the initial state of the cache may influence the number of cache hits and misses during program execution. In this paper, we study sensitivity properties of the relevant policies LRU, FIFO, and PLRU. To this end, we have developed a tool to precisely compute sensitivity properties for a large class of replacement policies. Our results suggest that the use of measurement may yield best- and worst-case execution time (BCET and WCET) estimates that are dramatically wrong.

Subproject(s): R2

Abstract (click to open/close)

Landmarks for propositional planning tasks are variable assignments that must occur at some point in every solution plan. We propose a novel approach for using landmarks in planning by deriving a pseudo-heuristic and combining it with other heuristics in a search framework. The incorporation of landmark information is shown to improve success rates and solution qualities of a heuristic planner. We furthermore show how additional landmarks and orderings can be found using the information present in multi-valued state variable representations of planning tasks. Compared to previously published approaches, our landmark extraction algorithm provides stronger guarantees of correctness for the generated landmark orderings, and our novel use of landmarks during search solves more planning tasks and delivers considerably better solutions.

Subproject(s): S1

Abstract (click to open/close)

Integrating agent programming languages and efficient action planning is a promising approach because it combines the expressive power of languages such as Golog with the possibility of searching for plans efficiently. In order to integrate a Golog interpreter with a planner, one has to understand, however, which part of the expressiveness of Golog can be captured by the planning language. Using Nebel's compilation framework, we identify a maximal fragment of basic action theories, the formalism Golog is based on, that is expressively equivalent to the ADL subset of PDDL. As we will show, almost all features that permit to specify incomplete information in basic action theories cannot be compiled to ADL.

Subproject(s): S1

Abstract (click to open/close)

The two central decision problems that arise during the design of safety critical systems are the satisfiability and the model checking problem. While model checking can only be applied after implementing the system, satisfiability checking answers the question whether a system that satisfies the specification exists. Model checking is traditionally considered to be the simpler problem -- for branching-time and fixed point logics such as CTL, CTL*, ATL, and the classical and alternating time mu-calculus, the complexity of satisfiability checking is considerably higher than the model checking complexity. We show that ATL* is a notable exception of this rule: Both ATL* model checking and ATL* satisfiability checking are 2EXPTIME-complete.

Subproject(s): S1,S2

Abstract (click to open/close)

The two central decision problems that arise during the design of safety critical systems are the satisfiability and the model checking problem. While model checking can only be applied after implementing the system, satisfiability checking answers the question whether a system that satisfies the specification exists. Model checking is traditionally considered to be the simpler problem - for branching-time and fixed point logics such as CTL, CTL*, ATL, and the classical and alternating time mu-calculus, the complexity of satisfiability checking is considerably higher than the model checking complexity. We show that ATL* is a notable exception of this rule: Both ATL* model checking and ATL* satisfiability checking are 2EXPTIME-complete.

Subproject(s): S1

Abstract (click to open/close)

This paper presents a novel strategy improvement algorithm for parity and payoff games, which is guaranteed to select, in each improvement step, an optimal combination of local strategy modifications. Current strategy improvement methods stepwise improve the strategy of one player with respect to some ranking function, using an algorithm with two distinct phases: They first choose a modification to the strategy of one player from a list of locally profitable changes, and subsequently evaluate the modified strategy. This separation is unfortunate, because current strategy improvement algorithms have no effective means to predict the global effect of the individual local modifications beyond classifying them as profitable, adversarial, or stale. Furthermore, they are completely blind towards the cross effect of different modifications: Applying one profitable modification may render all other profitable modifications adversarial. Our new construction overcomes the traditional separation between choosing and evaluating the modification to the strategy. It thus improves over current strategy improvement algorithms by providing the optimal improvement in every step, selecting the best combination of local updates from a superset of all profitable and stale changes.

Subproject(s): S1

Abstract (click to open/close)

This thesis offers a comprehensive solution of the distributed synthesis problem. It starts with the problem of solving Parity games, which form an integral part of the automata-theoretic synthesis algorithms we use. We improve the known complexity bound for solving parity games with n positions and c colors approximately from O(n^(c/2)) to O(n^(c/3)), and introduce an accelerated strategy improvement technique that can consider all combinations of local improvements in every update step, selecting the globally optimal combination. We then demonstrate the decidability and finite model property of alternating-time specification languages, and determine the complexity of the satisfiability and synthesis problem for the alternating-time mu-calculus and the temporal logic ATL*. The impact of the architecture, that is, the set of system processes with known (white-box) and unknown (black-box) implementation, and the communication structure between them, is determined. We introduce information forks, a simple but comprehensive criterion that characterizes all architectures for which the synthesis problem is undecidable. The information fork criterion takes the impact of nondeterminism, the communication topology, and the specification language into account. For decidable architectures, we present an automata-based synthesis algorithm. We introduce bounded synthesis, which deviates from general synthesis by considering only implementations up to a predefined size, and thus avoids the expensive representation of all solutions. We develop a SAT based approach to bounded synthesis, which is nondeterministic quasilinear in the minimal implementation instead of nonelementary in the system specification. We determine the complexity of open synthesis under the assumption of probabilistic or reactive environments. Our automata based approach allows for a seamless integration of the new environment models into the uniform synthesis algorithm. Finally, we study the synthesis problem for asynchronous systems. We show that distributed synthesis remains only decidable for architectures with a single black-box process, and determine the complexity of the synthesis problem for different scheduler types. Furthermore, we combine the undecidability results and synthesis procedures for synchronous and asynchronous systems; systems that are globally asynchronous and locally synchronous are decidable if all black-box components are contained in a single fork-free synchronized component.

Subproject(s): S1

Abstract (click to open/close)

In my diploma thesis, I discuss the theoretical background for a graphical user interface to model probabilistic hybrid automata and translate them to a stochastic satisfiability modulo theories problem in order to perform probabilistic bounded model checking. The tool which represents the practical part of this work is an extention to "HySAT GUI", a fronted for hybrid automata, developed during my individual project, supports not only simple probabilistic hybrid automata but systems of these. For the bounded model checking problem, in addition to simple state reachability, probabilistic verification of LTL-formulae is implemented. Altogether, this thesis deals with the translation of systems of probabilistic hybrid automata conjoined with either state reachability or a transformation of LTL-formulae to a bounded model checking problem as the target of a probabilistic bounded model checking problem. For the LTL-transformation, a symbolic and an automaton based approach are presented. As the result of the translation a predicative input language for the probabilistic bounded model checker SiSAT, currently developed in the scope of the AVACS project, is generated.

Subproject(s): H1/2,H4

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 solver and then removes the redundant constraints based on Craig interpolation. The approach is evaluated both for formulas from the model checking context including boolean combinations of linear constraints and boolean variables and for random trees composed of quantifiers, AND-, OR-, NOT-operators, and linear constraints produced by a generator. The results clearly show the advantages of our approach in comparison to state-of-the-art solvers.

Subproject(s): H3

Abstract (click to open/close)

We show that many properties studied in mathematical analysis (monotonicity, boundedness, inverse, Lipschitz properties, possibly combined with continuity or derivability) are expressible by formulae in a class for which sound and complete hierarchical proof methods for testing satisfiability of sets of ground clauses exist. The results are useful for automated reasoning in mathematical analysis and for the verification of hybrid systems.

Subproject(s): H3

Abstract (click to open/close)

We show that many properties studied in mathematical analysis (e.g. monotonicity, boundedness, inverse or Lipschitz properties, possibly combined with continuity and/or derivability) are expressible as axioms in a class for which sound and complete hierarchical proof methods for testing satisfiability of ground formulae exist. The results are useful for automated reasoning in analysis, and in the verification of hybrid systems.

Subproject(s): H3

Abstract (click to open/close)

In this paper we study interpolation in local extensions of a base theory. We identify situations in which it is possible to obtain interpolants in a hierarchical manner, by using a prover and a procedure for generating interpolants in the base theory as black-boxes. We present several examples of theory extensions in which interpolants can be computed this way, and discuss applications in verification, knowledge representation, and modular reasoning in combinations of local theories.

Subproject(s): R1,H3

Abstract (click to open/close)

In this paper we show that subsumption problems in many lightweight description logics (including cal EL) can be expressed as uniform word problems in classes of semilattices with monotone operators. We use possibilities of efficient local reasoning in such classes of algebras to obtain uniform PTIME decision procedures for CBox subsumption in cal EL and extensions thereof. These locality considerations allow us to present a new family of logics which extend cal EL with n-ary roles and numerical domains and also a new extension of cal EL^+.

Subproject(s): R1

Abstract (click to open/close)

In this paper we show that subsumption problems in many lightweight description logics (including cal EL) can be expressed as uniform word problems in classes of semilattices with monotone operators. We use possibilities of efficient local reasoning in such classes of algebras to obtain uniform PTIME decision procedures for CBox subsumption in cal EL and extensions thereof. These locality considerations allow us to present a new family of logics which extend cal EL and also a new extension of cal EL^+.

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 (where the topology expresses how the interacting systems share the information). This allows us to use results from categorical logic (and in particular geometric logic) to describe which type of properties are transferred, if valid locally in all component systems, also at a global level, to the system obtained by interconnecting the individual systems. The main area of application is to modular verification of complex systems. We illustrate the ideas by means of an example involving a family of interacting controllers for trains on a rail track.

Subproject(s): R1

Abstract (click to open/close)

We investigate reachability (or equivalently, safety) for timed systems modelled as Timed Automata (TA) under notions of “robustness”, i.e., when the clocks of the TA may drift by small amounts. Our contributions are two-fold: (1) We first consider the model of clock-drift introduced by Puri [1] and subsequently studied in other works [2,3,4]. We show that the standard zone-based forward reachability analysis performed by tools such as UPPAAL is in fact exact for TA with closed guards, invariants, and targets, when testing robust safety of timed systems having an arbitrary, but finite lifetime. (2) Next, we consider a more realistic model of drifting clocks that takes into account the regular resynchronization performed in most practical systems. We then show that the standard reachability analysis of tools like UPPAAL again suffices to test for robust safety in this model of clock-drift, for TA with closed guards, invariants, and targets, but now without any restrictions on system life-time.

Subproject(s): R1

Abstract (click to open/close)

The stochastic satisfiability modulo theories (SSMT) problem is a generalization of the SMT problem on existential and randomized (aka. stochastic) quantification over discrete variables of an SMT formula. This extension permits the concise description of diverse problems combining reasoning under uncertainty with data dependencies. Solving problems with various kinds of uncertainty has been extensively studied in Artificial Intelligence. Famous examples are stochastic satisfiability and stochastic constraint programming. In this paper, we extend the algorithm for SSMT for decidable theories presented in [FHT08] to non-linear arithmetic theories over the reals and integers which are in general undecidable. Therefore, we combine approaches from Constraint Programming, namely the iSAT algorithm tackling mixed Boolean and non-linear arithmetic constraint systems, and from Artificial Intelligence handling existential and randomized quantifiers. Furthermore, we evaluate our novel algorithm and its enhancements on benchmarks from the probabilistic hybrid systems domain.

Subproject(s): H1/2,H4

Abstract (click to open/close)

The recently presented constraint solver HySAT tackles the in general undecidable problem of solving mixed Boolean and non-linear arithmetic constraint formulae over the reals involving transcendental functions. The algorithmic core of HySAT is the iSAT algorithm, a tight integration of the Davis-Putnam-Logemann-Loveland algorithm with interval constraint propagation enriched by enhancements like conflict-driven clause learning and non-chronological backtracking. However, it was an open question whether HySAT's conflict analysis scheme, an adapted first unique implication point technique as applied in most modern SAT solvers, performs favorably compared to other schemes. In this paper, we compare several conflict analysis heuristics to answer this question. Furthermore, we consider the integration of restarts into the iSAT algorithm and investigate their impact. For our empirical results we use benchmarks from the hybrid systems domain.

Subproject(s): H1/2

Abstract (click to open/close)

This paper addresses the formal verification of distributed systems comprising a dynamically changing and potentially unbounded number of processes. We employ the spotlight principle to obtain a concise finitary abstraction of the system and devise an abstraction refinement strategy guided by the analysis of abstract counterexamples. It turns out that the key problem for spotlight refinement is the identification of spurious counterexamples. We observe that the problem is in general undecidable, and provide a sound but incomplete method that is able to solve the problem for many practically relevant systems. Our method is driven by a three-valued satisfaction relation for temporal specifications that accounts for the fact that concrete counterexamples can be identified in the abstracted system if they occur within the spotlight.

Subproject(s): S2

Abstract (click to open/close)

Planning as heuristic search is a powerful approach to solving domain independent planning problems. In recent years, various successful heuristics and planners like textsc FF, textsc LPG, textsc Fast Downward or textsc SGPlan have been proposed in this context. However, as heuristics only estimate the distance to goal states, a general problem of heuristic search is the existence of plateaus in the search space topology which can cause the search process to degenerate. Additional techniques like helpful actions or preferred operators that evaluate the ``usefulness'' of actions are often successful strategies to support the search in such situations. In this paper, we introduce a general method to evaluate the usefulness of actions. We propose a technique to enhance heuristic search by identifying ``useless'' actions that are not needed to find optimal plans. In contrast to helpful actions or preferred operators that are specific to the FF and Causal Graph heuristic, respectively, our method can be combined with arbitrary heuristics. We show that this technique often yields significant performance improvements.

Subproject(s): R3

Abstract (click to open/close)

Directed model checking is a well-established technique that computes an abstract distance function in order to guide the state space traversal towards error states. In this paper, we introduce the concept of useless transitions. We introduce a method, parametrized by the abstract distance function, to recognize relatively useless transitions. We define a corresponding new strategy for the state space traversal. We have implemented the overall method. Preliminary experiments indicate its practical potential. Apparently the new method identifies a sweetspot in the trade-off between scalability (memory consumption) and short computed error traces.

Subproject(s): R3

Subproject(s): R2

Abstract (click to open/close)

Bisimulation minimization is one of the classical means to fight the infamous state space explosion problem in verification. Particularly in stochastic verification, numerical algorithms are applied, which do not scale beyond systems of moderate size. To alleviate this problem, symbolic bisimulation minimization has been used effectively to reduce very large symbolically represented state spaces to moderate size explicit representations. But even this minimization may fail due to time or memory limitations. This paper presents a symbolic algorithm which relies on a hybrid symbolic partition representation. It dynamically converts between two known representations in order to provide a trade-off between memory consumption and runtime. The conversion itself is logarithmic in the partition size. We show how to apply it for the minimization of Markov chains, but the same techniques can be adapted in a straightforward way to other models like labeled transition systems or interactive Markov chains.

Subproject(s): S3

Abstract (click to open/close)

For formal verification, reliable results are of utmost importance. In model checking of digital systems, mainly incorrect implementations due to logical errors are the source of wrong results. In probabilistic model checking, however, numerical instabilities are an additional source for inconsistent results.

First we present an example, for which several state-of-the-art probabilistic model checking tools give completely wrong results due to inexact computations. This motivates the investigation at which points inaccuracies are introduced during the model checking process. We then give ideas how, in spite of these inaccuracies, reliable results can be obtained or at least the user be warned about potential problems: (1) to introduce a ``degree of belief'' for each sub-formula, (2) to use exact (rational) arithmetic, (3) to use interval arithmetic to obtain safe approximations of the actual probabilities, and (4) to provide certificates which testify that the result is correct.

Subproject(s): S3

Abstract (click to open/close)

In formal verification, reliable results are of utmost importance. In model checking of digital systems, mainly incorrect implementations of the model checking algorithms due to logical errors are the source of wrong results. In probabilistic model checking, however, numerical instabilities are an additional source for inconsistent results.

We motivate our investigations with an example, for which several state-of-the-art probabilistic model checking tools give completely wrong results due to inexact computations. We then analyze, at which points inaccuracies are introduced during the model checking process. We discuss first ideas how, in spite of these inaccuracies, reliable results can be obtained or at least the user be warned about potential correctness problems: (1) usage of exact (rational) arithmetic, (2) usage of interval arithmetic to obtain safe approximations of the actual probabilities, (3) provision of certificates which testify that the result is correct, and (4) integration of a ``degree of belief'' for each sub-formula into existing model checking tools.

Subproject(s): S3

Abstract (click to open/close)

Das Lösen von Constraint-Systemen ist für sicherheitskritische Systeme eine wichtige Methode, um kritische Zustände aufzudecken oder das Ausbleiben von Fehlern zu belegen. In der Arbeit [FHR+07] wird der iSAT-Algorithmus vorgestellt, der solche Constraint-Systeme mit komplexer boolescher Struktur und potentiell nicht-linearen arithmetischen Constraints löst. Durch die Komplexität der Probleme wird das Vorgehen dieses Algorithmus unüberschaubar. In dieser Arbeit wird das Visualisierungstool iSATVis vorgestellt, welches in diversen Darstellungsmodi, beispielsweise der Häufigkeitsanalyse und dem Abhängigkeitsgraphen, mit unterschiedlichen Perspektiven die interne Struktur eines Solving-Prozesses veranschaulichen kann. Damit werden Besonderheiten von modellierten Problemen sichtbar, so dass ein besseres Verständnis über den Solver aufgebaut wird. [FHR+07]: Fränzle et.al. ``Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure'', JSAT Special Issue on Constraint Programming and SAT, Vol.1, pp.209-236, 2007

Subproject(s): H1,H2

Abstract (click to open/close)

The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are widely used models for concurrent system designs making it possible to model check such properties. In this paper, we focus on probabilistic timing properties of infinite-state CTMCs, expressible in continuous stochastic logic (CSL). Such properties comprise important dependability measures, such as timed probabilistic reachability, performability, survivability, and various availability measures like instantaneous availabilities, conditional instantaneous availabilities and interval availabilities. Conventional model checkers explore the given model exhaustively which is not always possible either due to state explosion or because the model is infinite. This paper presents a method that only explores the infinite (or prohibitively large) model up to a finite depth, with the depth bound being computed on-the-fly. We provide experimental evidence showing that our method is effective.

Subproject(s): S3

Abstract (click to open/close)

Bounded Model Checking (BMC) is a successful refutation method to detect errors in not only circuits and other binary systems but also in systems with more complex domains like timed automata or linear hybrid automata. Counterexamples of a fixed length are described by formulas in a decidable logic, and checked for satisfiability by a suitable solver. In an earlier paper we analyzed how BMC of linear hybrid automata can be accelerated already by appropriate encoding of counterexamples as formulas and by selective conflict learning. In this paper we introduce parametric datatypes for the internal solver structure that, taking advantage of the symmetry of BMC problems, remarkably reduce the memory requirements of the solver.

Subproject(s): H2

Abstract (click to open/close)

We present GDPLL, a generalization of the DPLL procedure. It solves the satisfiability problem for decidable fragments of quantifier free first-order logic. Sucient conditions are identified for proving soundness, termination and completeness of GDPLL. We show how the original DPLL procedure is an instance. Subsequently the GDPLL instances for equality logic, and the logic of equality over infinite ground term algebras are presented. Based on this, we implemented a decision procedure for inductive datatypes. We provide some new benchmarks, in order to compare variants.

Keywords: satisfiability, DPLL procedure, equality, ground term algebra, inductive datatypes, decision procedure
Subproject(s): H1,H2

Subproject(s): S1

Subproject(s): S2

Abstract (click to open/close)

On the basis of a case-study, we demonstrate the usefulness of topology invariants for model-driven systems development. Considering a graph grammar semantics for a relevant fragment of UML, where a graph represents an object diagram, allows us to apply Topology Analysis, a particular abstract interpretation of graph grammars. The outcome of this analysis is a finite and concise over-approximation of all possible reachable object diagrams, the so-called topology invariant. We discuss how topology invariants can be used to verify that constraints on a given model are respected by the behaviour and how they can be viewed as synthesised constraints providing insight into the dynamic behaviour of the model.

Subproject(s): S2

Abstract (click to open/close)

On the basis of a case-study, we demonstrate the usefulness of topology invariants for model-driven systems development. Considering a graph grammar semantics for a relevant fragment of UML, where a graph represents an object diagram, allows us to apply Topology Analysis, a particular abstract interpretation of graph grammars. The outcome of this analysis is a finite and concise description of reachable object diagram, the so-called topology invariant. We discuss how topology invariants can be used to verify that constraints on a given model are respected by the behaviour and how they can be viewed as synthesised constraints providing insight into the dynamic behaviour of the model.

Subproject(s): S2

Abstract (click to open/close)

Dynamic Communication Systems (DCS) are infinite state systems where an unbounded number of processes operate in an evolving communication topology. For automated verification of properties of DCS, finitary abstractions based on exploiting symmetry can be employed. However, these abstractions give rise to spurious behaviour that often inhibits to successfully prove relevant properties. In this paper, we propose to combine a particular finitary abstraction with global system invariants obtained by abstract interpretation. These system invariants establish an over-approximation of possible communication topologies occurring at runtime, which can be used to identify and exclude spurious behaviour introduced by the finitary abstraction, which is thereby refined. Based on a running example of car platooning, we demonstrate that our approach allows to verify temporal DCS properties that no technique in isolation is able to prove.

Subproject(s): S2

Abstract (click to open/close)

Dynamic Communication Systems (DCS) are infinite state systems where an unbounded number of processes operate in an evolving communication topology. For automated verification of properties of DCS, finitary abstractions based on exploiting symmetry can be employed. However, these abstractions give rise to spurious behaviour that often inhibits to successfully prove relevant properties. In this paper, we propose to combine a particular finitary abstraction with global system invariants obtained by abstract interpretation. These system invariants establish an over-approximation of possible communication topologies occurring at runtime, which can be used to identify and exclude spurious behaviour introduced by the finitary abstraction, which is thereby refined. Based on a running example of car platooning, we demonstrate that our approach allows to verify temporal DCS properties that no technique in isolation is able to prove.

Subproject(s): S2

Abstract (click to open/close)

An interesting class of systems is characterised by a changing and potentially unbounded number of processes. Prominent instances are ad-hoc networks, dynamic communication systems, and object-oriented programs. Properties of such systems are naturally specified by predicative variants of temporal logic. So a number of logics have been proposed. However, the proposals are inconsistent among each other and lack a common understanding of the underlying systems. In this article, we comprehensively identify features whose characteristics determine the design of such logics. Given dynamic object creation and destruction, it turns out that the most crucial feature is that of disappearance. That is, how does a formula evaluate if its actors disappear? While some approaches avoid this problem at all, we propose a generalised logic subsuming the existing ones. We show that our proposal conservatively extends propositional temporal logic and conduct first investigations of emerging new issues of such temporal logics.

Subproject(s): S2

Abstract (click to open/close)

The Transregional Collaborative Research Center AVACS integrates the three sites Freiburg, Oldenburg, and Saarbr�cken and addresses the challenge of pushing the borderline for automatic verification and analysis of complex systems. A particular focus of the project is on models of complex transportation systems and their safety requirements. AVACS is organized in ten subprojects, each teaming researchers from all sites, and is funded by the German Science Foundation since January 1, 2004. This articles surveys scope, organization and research directions of AVACS, including pointers to key publications.

Subproject(s): R1,R2,R3,H1,H2,H3,H4,S1,S2,S3

Abstract (click to open/close)

We present the tool LIRA that implements decision procedures based on automata-theoretic techniques for first-order logics with linear arithmetic over the integers and the reals. LIRA also provides an efficient automata library, which is accessible through a high-level and low-level API.

Subproject(s): H1

Abstract (click to open/close)

In polyhedral studies of 0/1 polytopes two prominent problems exist. One is the vertex enumeration problem: Given a system of inequalities, enumerate its feasible 0/1 points. Another one is the convex hull problem: Given a set of 0/1 points in dimension d, enumerate the facets of the corresponding polytope. We present two new approaches for both problems. The novelty of our algorithms is the incorporation of binary decision diagrams (BDDs), a datastructure which has become very popular and effective in hardware verification and computational logic. Our computational results show the strength of our methods. We introduce our new tool azove which is currently the fastest software for counting and enumerating 0/1 points in a polytope.

Subproject(s): H2

Abstract (click to open/close)

We propose a shape analysis that adapts to some of the complex composite data structures found in industrial systems-level programs. Examples of such data structures include "cyclic doubly-linked lists of acyclic singly-linked lists", "singly-linked lists of cyclic doubly-linked lists with back-pointers to head nodes", etc. The analysis introduces the use of generic higher-order inductive predicates describing spatial relationships together with a method of synthesizing new parameterized spatial predicates which can be used in combination with the higher-order predicates. In order to evaluate the proposed approach for realistic programs we have performed experiments on examples drawn from device drivers: the analysis proved safety of the data structure manipulation of several routines belonging to an IEEE 1394 (firewire) driver, and also found several previously unknown memory safety bugs.

Subproject(s): S2

Abstract (click to open/close)

We present a constraint-based algorithm for the synthesis of invariants expressed in the combined theory of linear arithmetic and uninterpreted function symbols. Given a set of programmer-specified invariant templates, our algorithm reduces the invariant synthesis problem to a sequence of arithmetic constraint satisfaction queries. Since the combination of linear arithmetic and uninterpreted functions is a widely applied predicate domain for program verification, our algorithm provides a powerful tool to statically and automatically reason about program correctness. The algorithm can also be used for the synthesis of invariants over arrays and set data structures, because satisfiability questions for the theories of sets and arrays can be reduced to the theory of linear arithmetic with uninterpreted functions. We have implemented our algorithm and used it to find invariants for a low-level memory allocator written in C.

Subproject(s): R1

Abstract (click to open/close)

The success of software verification depends on the ability to find a suitable abstraction of a program automatically. We propose a method for automated abstraction refinement which overcomes some limitations of current predicate discovery schemes. In current schemes, the cause of a false alarm is identified as an infeasible error path, and the abstraction is refined in order to remove that path. By contrast, we view the cause of a false alarm?the spurious counterexample?as a full-fledged program, namely, a fragment of the original program whose control-flow graph may contain loops and represent unbounded computations. There are two advantages to using such path programs as counterexamples for abstraction refinement. First, we can bring the whole machinery of program analysis to bear on path programs, which are typically small compared to the original program. Specifically, we use constraint-based invariant generation to automatically infer invariants of path programs ?so-called path invariants. Second, we use path invariants for abstraction refinement in order to remove not one infeasibility at a time, but at once all (possibly infinitely many) infeasible error computations that are represented by a path program. Unlike previous predicate discovery schemes, our method handles loops without unrolling them; it infers abstractions that involve universal quantification and naturally incorporates disjunctive reasoning.

Subproject(s): R1

Subproject(s): S3

Abstract (click to open/close)

Dynamic Fault Trees (DFT) extend standard fault trees by allowing the modeling of complex system components' behaviors and interactions. Being a high level model and easy to use, DFT are experiencing a growing success among reliability engineers. Unfortunately, a number of issues still remains when using DFT. Briefly, these issues are (1) a lack of formality (syntax and semantics), (2) limitations in modular analysis and thus vulnerability to the state-space explosion problem, and (3) lack in modular model-building. We use the input/output interactive Markov chain (I/O-IMC) formalism to analyse DFT. I/O-IMC have a precise semantics and are an extension of continuous-time Markov chains with input and output actions. In this paper, using the I/O-IMC framework, we address and resolve issues (2) and (3) mentioned above. We also show, through some examples, how one can readily extend the DFT modeling capabilities using the I/O-IMC framework.

Subproject(s): S3

Abstract (click to open/close)

This paper presents our integration of efficient resolution-based theorem provers into the Jahob data structure verification system. Our experimental results show that this approach enables Jahob to automatically verify the correctness of a range of complex data structures, including data structures such as hash tables and search trees, without the need for interative theorem proving or techniques tailored to individual data structures. Our primary technical results include: (1) a translation from higher-order logic to first-order logic that enables the application of resolution-based theorem provers and (2) a proof that eliminating type (sort) information in formulas is both sound and complete, even in the presence of a generic equality operator. Moreover, our experimental results show that the elimination of this type information dramatically decreases the time required to prove the resulting formulas. These techniques enabled us to verify complex correctness properties of Java programs such as a mutable set implemented as an imperative linked list, a finite map implemented as a functional ordered tree, a hash table with a mutable array, and a simple library system example that uses these container data structures. Our system verifies (in a matter of minutes) that data structure operations correctly update the finite map, that they preserve data structure invariants (such as ordering of elements, membership in appropriate hash table buckets, or relationships between sets and relations), and that there are no run-time errors such as null dereferences or array out of bounds accesses.

Subproject(s): S2

Abstract (click to open/close)

The high-level specification language CSP-OZ-DC has been shown to be well-suited for modelling and analysing industrially relevant concurrent real-time systems. It allows to model each of the most important functional aspects such as control flow, data, and real-time requirements in adequate notations, maintaining a common semantical foundation for subsequent verification. Slicing on the other hand has become an established technique to complement the fight against state space explosion during verification which inherently accompanies increasing system complexity. In this paper, we exploit the special structure of CSP-OZ-DC specifications by extending the dependence graph--which usually serves as a basis for slicing--with several new types of dependencies, including timing dependencies derived from the specification's DC part. Based on this we show how to compute a specification slice and prove correctness of our approach.

Subproject(s): R1

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)

We formulate the problem of estimating the region of attraction using quantified constraints and show how the resulting constraints can be solved using existing software packages. We discuss the advantages of the resulting method in detail.

Keywords: region of attraction, constraint solving
Subproject(s): H4

Abstract (click to open/close)

In recent years we have seen great progress made in the area of automatic source-level static analysis tools. However, most of today?s program verification tools are limited to properties that guarantee the absence of bad events (safety properties). Until now no formal software analysis tool has provided fully automatic support for proving properties that ensure that good events eventually happen (liveness properties). In this paper we present such a tool, which handles liveness properties of large systems written in C. Liveness properties are described in an extension of the specification language used in the SDV system. We have used the tool to automatically prove critical liveness properties of Windows device drivers and found several previously unknown liveness bugs.

Subproject(s): H4

Abstract (click to open/close)

Concurrent programs are often designed such that certain functions executing within critical threads must terminate. Examples of such cases can be found in operating systems, web servers, email clients, etc. Unfortunately, no known automatic program termination prover supports a practical method of proving the termination of threads. In this paper we describe such a procedure. The procedure?s scalability is achieved through the use of environment models that abstract away the surrounding threads. The procedure?s accuracy is due to a novel method of incrementally constructing environment abstractions. Our method finds the conditions that a thread requires of its environment in order to establish termination by looking at the conditions necessary to prove that certain paths through the thread represent well-founded relations if executed in isolation of the other threads. The paper gives a description of experimental results using an implementation of our procedure on Windows device drivers, and a description of a previously unknown bug found with the tool.

Subproject(s): H4

Abstract (click to open/close)

We propose algorithms significantly extending the limits for maintaining exact representations in the verification of linear hybrid systems with large discrete state spaces. We use AND-Inverter Graphs (AIGs) extended with linear constraints ( Laig s) as symbolic representation of the hybrid state space, and show how methods for maintaining compactness of AIGs can be lifted to support model-checking of linear hybrid systems with large discrete state spaces. This builds on a novel approach for eliminating sets of redundant constraints in such rich hybrid state representations by a suitable exploitation of the capabilities of SMT solvers, which is of independent value beyond the application context studied in this paper. We used a benchmark derived from an Airbus flap control system (containing 2²⁰ discrete states) to demonstrate the relevance of the approach.

Subproject(s): H3

Abstract (click to open/close)

We propose algorithms significantly extending the limits for maintaining exact representations in the verification of linear hybrid systems with large discrete state spaces. We use AND-Inverter Graphs (AIGs) extended with linear constraints (LinAIGs) as symbolic representation of the hybrid state space, and show how methods for maintaining compactness of AIGs can be lifted to support model-checking of linear hybrid systems with large discrete state spaces. This builds on a novel approach for eliminating sets of redundant constraints in such rich hybrid state representations by a suitable exploitation of the capabilities of SMT solvers, which is of independent value beyond the application context studied in this paper. We used a benchmark derived from an Airbus flap control system (containing 2^20 discrete states) to demonstrate the relevance of the approach.

Subproject(s): H3

Abstract (click to open/close)

We present a verification methodology for cooperating traffic agents covering analysis of cooperation strategies, realization of strategies through control, and implementation of control. For each layer, we provide dedicated approaches to formal verification of safety and stability properties of the design. The range of employed verification techniques invoked to span this verification space includes application of pre-verified design patterns, automatic synthesis of Lyapunov functions, constraint generation for parameterized designs, model-checking in rich theories, and abstraction refinement. We illustrate this approach with a variant of the European Train Control System (ETCS), employing layer specific verification techniques to layer specific views of an ETCS design.

Subproject(s): H3

Subproject(s): H3,H4

Abstract (click to open/close)

The Live Sequence Charts (LSC) language is a formally rigorous variant of the well-known scenario language Message Sequence Charts (MSC). LSCs yield expressive power by means to distinguish mandatory and scenario behaviour, means to characterise by another scenario the context in which a specification applies, and means to distinguish required from possible progress, i.e. to require liveness. From the original proposal by Damm and Harel [1], two slightly different dialects emerged, one in the context of LSC play-in and -out [2] and one for the use of LSCs as formal, model-based approaches to software development [3]. In this paper, we investigate the expressive power of LSCs in the sense of [3]. That is, we first (constructively) show that for each LSC there is an equivalent CTL* formula. Complementing existing work, we show that the containment is strict, that is, not each CTL* formula has an equivalent LSC. To complete the discussion, we present for the first time a way back, from a syntactically characterised fragment of CTL* to the subset of bonded LSC specifications, thereby establishing an equivalence.

Subproject(s): S2

Abstract (click to open/close)

Automata over infinite words provide a powerful framework to solve various decision problems. However, the mechanized reasoning with restricted classes of automata over infinite words is often simpler and more efficient. For instance, weak deterministic B�chi automata (WDBAs) can be handled algorithmically almost as efficient as deterministic automata over finite words. In this paper, we show how and when the standard powerset construction for automata over finite words can be used to determinize automata over infinite words. An instance is the class of automata that accept WDBA-recognizable languages. Furthermore, we present applications of this new determinization construction. Namely, we apply it to improve the automata-based approach for the mixed first-order linear arithmetic over the reals and the integers, and we utilize it to accelerate finite state model checking. We report on experimental results for these two applications.

Subproject(s): H1,H2

Abstract (click to open/close)

We present a fully automatic approach for counter-example guided abstraction refinement of real-time systems modelled in a subset of timed automata. Our approach is implemented in the Moby/RT tool environment, which is a CASE tool for embedded system specifications. Verification in Moby/RT is done by constructing abstractions of the semantics in terms of timed automata which are fed into the model checker UPPAAL. Since the abstractions are over-approximations, absence of abstract counter-examples implies a valid result for the full model. Our new approach deals with the situation in which an abstract counter-example is found by UPPAAL. The generated abstract counter-example is used to construct either a concrete counter-example for the full model or to identify a slightly refined abstraction in which the found spurious counter-example cannot occur anymore. Hence, the approach allows for a fully automatic abstraction refinement loop starting from the coarsest abstraction towards an abstraction for which a valid verification result is found. Nontrivial case studies demonstrate that this approach computes small abstractions fast without any user interaction.

Abstract (click to open/close)

Combinational equivalence checking is an essential task in circuit design. In this paper we focus on SAT based equivalence checking making use of incremental SAT techniques which are well known from the application inBounded Model Checking. Based on an analysis of shared circuit structures we present heuristics which try to maximize the benefit from incremental SAT solving in this application by looking for good orders in which the equivalence of different circuit outputs is checked. Moreover, we present a reset strategy for situations where the benefit from the incremental SAT approach seems to decrease. Experimental results prove that our novel method outperforms traditional methods significantly.

Subproject(s): H3

Subproject(s): R3

Abstract (click to open/close)

In the design process of real-time systems, formal verification establishes global properties of high-level specifications while real-time scheduling analysis ensures that concrete realisations meet essential timing properties with respect to a given target platform. But a formal link between these phases is missing. It is unclear (1) whether timing assumptions that are required to verify properties of high-level specifications can actually be realised on a target platform and (2) whether verified properties remain valid for a schedulable task network. Our approach bridges this gap by guaranteeing that properties verified on specification level are preserved on the implementation level, and vice versa, schedulability results can be propagated back to the specification. To this end, we provide a property-preserving translation from a subclass of the high-level real-time language CSP-OZ-DC into Cyclic Timed Automata, a Timed Automata based task network formalism. We apply our method to a case study from the European Train Control System standard.

Subproject(s): R1,R2

Abstract (click to open/close)

We extend existing verification methods for CSP-OZ-DC to reason about real-time systems with complex data types and timing parameters. We show that important properties of systems can be encoded in well-behaved logical theories in which hierarchical reasoning is possible. Thus, testing invariants and bounded model checking can be reduced to checking satisfiability of ground formulae over a simple base theory. We illustrate the ideas by means of a simplified version of a case study from the European Train Control System standard.

Subproject(s): R1

Abstract (click to open/close)

The worst-case execution time analyzer aiT originally developed by Saarland University and AbsInt GmbH computes safe and precise upper bounds for the WCETs of tasks. It relies on a pipeline model that usually has been handcrafted.We present some new approaches aiming at automatically obtaining a pipeline model as required by aiT from a formal processor description in VHDL or Verilog. The derivation of the total WCET from the basic-block WCETs requires knowledge about upper bounds on the number of loop iterations. We present a new method for loop bound detection using dataflow analysis to derive loop invariants. A task may contain infeasible paths caused by conditionals with logically related conditions. We present a static analysis that identifies and collects conditions from the executable, and relates these collections to detect infeasible paths. This new analysis uses the results of a novel generic slicer on the level of binary code.

Subproject(s): R2

Abstract (click to open/close)

We apply SMT solving to synthesize distributed systems from specifications in linear-time temporal logic (LTL). The LTL formula is translated into an equivalent universal co-Buchi tree automaton. The existence of a finite transition system in the language of the automaton is then specified as a quantified formula in the theory (N,<) of the ordered natural numbers with uninterpreted function symbols. While our experimental results indicate that the resulting satisfiability problem is generally out of reach for the currently available SMT solvers, the problem immediately becomes tractable if we fix an upper bound on the number of states in the distributed system. After replacing each universal quantifier by an explicit conjunction, the SMT solver Yices solves simple single-process synthesis problems within a few seconds, and distributed synthesis problems, such as a two-process distributed arbiter, within one minute.

Subproject(s): S1

Abstract (click to open/close)

A decidability result and a model-checking procedure for a rich subset of Duration Calculus (DC) [19] is obtained through reductions to is obtained through reductions to First-order logic over the real-closed field and to Multi-Priced Timed Automata (MPTA) [13]. In contrast to other reductions of fragments of DC to reachability problems in timed automata, the reductions do also cover constraints on positive linear combinations of accumulated durations. By being able to handle accumulated durations under chop as well as in arbitrary positive Boolean contexts, the procedures extend the results of Zhou et al. [22] on decidability of linear duration invariants to a much wider fragment of DC.

Keywords: Real-time systems, metric-time temporal logic, decidability, model-checking, multi-priced timed automata
Subproject(s): H1

Abstract (click to open/close)

In this paper we present HySAT, a new bounded model checker for linear hybrid systems, incorporating a tight integration of a DPLL-based pseudo-Boolean SAT solver and a linear programming routine as core engine. In contrast to related tools like MathSAT, ICS, or CVC, our tool exploits all of the various optimizations that arise naturally in the bounded model checking context, e.g. isomorphic replication of learned conflict clauses or tailored decision strategies, and extends them to the hybrid domain. We demonstrate that those optimizations are crucial to the performance of the tool.

Keywords: verification, bounded model checking, hybrid systems, infinite-state systems, decision procedures, satisfiability
Subproject(s): H2

Abstract (click to open/close)

In order to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving transcendental functions, we provide a tight integration of recent SAT solving techniques with interval-based arithmetic constraint solving. Our approach deviates substantially from lazy theorem proving approaches in that it directly controls arithmetic constraint propagation from the SAT solver rather than delegating arithmetic decisions to a subordinate solver. Through this tight integration, all the algorithmic enhancements that were instrumental to the enormous performance gains recently achieved in propositional SAT solving do smoothly carry over to the rich domain of non-linear arithmetic constraints. As a consequence, our approach is able to handle large constraint systems with extremely complex Boolean structure, involving Boolean combinations of multiple thousand arithmetic constraints over some thousands of variables.

Subproject(s): H1,H2

Abstract (click to open/close)

Given the structural diversity of modeling paradigms for hybrid systems that are in widespread use, which ranges from a signal-transducer-based view like in Simulink/Stateflow to an automaton-based view in various hybrid automata frameworks, there is need for an intermediate-level language that can accommodate these structures in a concise way, thereby isolating verification backends from the particular modeling frontend used. This technical report provides a description of the intermediate-level modeling language for hybrid systems used in project area H of AVACS as a gateway to verification backends.

Subproject(s): H1/2,H3

Abstract (click to open/close)

Most recent embedded systems use caches to improve their average performance. Current timing analyses are able to compute safe timing guarantees for these systems, if tasks are running to completion. If preemptive scheduling is enabled, the previously computed timing guarantees no longer hold. At each program point, a preempting task might completely change the cache content. This observation has to be considered by timing analyses, which inevitably increases their complexity. Additionally, these cache-interferences influence the overall performance of such systems. The position of a task?s data determines the portion of the cache the task will occupy, and by this, the cache-interferences of the different tasks. In this paper, we present a novel method that computes an optimal taskset placement with respect to the above criteria. This means, our method modifies the starting addresses of the tasks such that the number of persistent task sets is maximized for each task. We show that the problem of finding an optimal placement is NP-hard and present a heuristic to approximate an optimal solution. Finally, we demonstrate by means of simulations that our method is able to improve the overall performance especially of heterogeneous and complex tasksets.

Abstract (click to open/close)

Wireless embedded sensor networks are predicted to provide attractive application possibilities in industry as well as at home. IEEE 802.15.4 and ZigBee are proposed as standards for such networks with a particular focus on pairing reliability with energy efficiency, while sacrificing high data rates. IEEE 802.15.4 is configurable in many aspects, including the synchronicity of the communication, and the periodicity in which battery-powered sensors need to wake up to communicate. This paper develops a formal behavioral model for the energy implications of these options. The model is modularly specified using the language MoDeST, which has an operational semantics mapping on stochastic timed automata. The latter are simulated using a variant of discrete-event simulation implemented in the tool Möbius. We obtain estimated energy consumptions of a number of possible communication scenarios in accordance with the standards, and derive conclusions about the energy-optimal configuration of such networks. As a specific fine point, we investigate the effects of drifting clocks on the energy behaviour of various application scenarios.

Keywords: sensor network, energy consumption, ZigBee, stochastic modelling
Subproject(s): S3

Subproject(s): R3

Abstract (click to open/close)

We describe an approach to deriving consistent heuristics for automated planning, based on explicit search in abstract state spaces. The key to managing complexity is interleaving composition of abstractions over different sets of state variables with abstraction of the partial composites. The approach is very general and can be instantiated in many different ways by following different abstraction strategies. In particular, the technique subsumes planning with pattern databases as a special case. Moreover, with suitable abstraction strategies it is possible to derive perfect heuristics in a number of classical benchmark domains, thus allowing their optimal solution in polynomial time. To evaluate the practical usefulness of the approach, we perform empirical experiments with one particular abstraction strategy. Our results show that the approach is competitive with the state of the art.

Subproject(s): R3

Abstract (click to open/close)

In this paper we discuss a formalization for combining 01X-logic and quantified boolean formulas (QBF) within a homogeneous SAT-framework. The motivation for this approach stems from bounded model checking of blackbox designs where 01X-logic and QBFs where already successfully applied, but still in a separate manner. The proposed combination allows a more flexible handling of blackboxes depending on the problem under analysis.

Subproject(s): S1

Abstract (click to open/close)

One approach for the verification of embedded systems, where discrete control is embedded in a continuous environment, is bounded model checking of linear hybrid automata. As a decision procedure within this context, a combination of a propositional SAT-solver and an LP-solver can be used. For such combined SAT-LP solvers, it is, among others, an open question how a robust, i.e., reliable, variable selection heuristics should be designed. In this work we investigate the design of such heuristics taking into account (1) the algorithmic structure of the combined SAT-LP-solver, and (2) efficiency issues in form of a counter-based design that adapts the popular concept of the VSIDS heuristics of Chaff. An empirical analysis of our framework shows (1) the importance of guard variables related to real-valued constraints and (2) reveals an ambiguity between the number of calls of the LP-solver and the time used by the LP-solver. As a result, we propose a simple, but efficient, variable selection heuristics that takes our observations into account and experimentally overcomes the limitations of existing ones.

Subproject(s): H2

Abstract (click to open/close)

In the past, we have investigated satisfiability-based combinational equivalence checking and bounded model checking of partial circuit designs, i.e., circuit designs where one or more components of the design are not implemented yet. Especially for satisfiability-based bounded model checking, typically a counterexample is generated in case that the specification property is violated. Minimizing the number of assigned variables in the satisfying assignment that corresponds to such a counterexample is the objective of lifting. In this work we show that lifting is also feasible and profitable for counterexamples obtained via satisfiability-based bounded model checking of partial designs. We provide first experimental results on this issue that show its feasibility. Furthermore, we present a novel application scenario for lifting in the context of automated blackbox synthesis. This is a useful concept that can be applied during combinational equivalence checking of partial circuit designs, where realizability of the missing components was already proven, but the functionality of the missing components is still unknown. As a summary, this work provides first experimental results as well as a novel concept regarding the application of lifting for the analysis of partial designs.

Subproject(s): S1

Abstract (click to open/close)

Continuous-time Markov decision processes (CTMDPs) are behavioral models with continuous-time, nondeterminism and memoryless stochastics. Recently, an efficient timed reachability algorithm for CTMDPs has been presented, allowing one to quantify, e. g., the worst-case probability to hit an unsafe system state within a safety critical mission time. This algorithm works only for uniform CTMDPs -- CTMDPs in which the sojourn time distribution is unique across all states. In this paper we develop a compositional theory for generating CTMDPs which are uniform by construction. To analyze the scalability of the method, this theory is applied to the construction of a fault-tolerant workstation cluster example, and experimentally evaluated using an innovative implementation of the timed reachability algorithm. All previous attempts to model-check this seemingly well-studied example needed to ignore the presence of nondeterminism, because of lacking support for modelling and analysis.

Subproject(s): S3

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 and practical tradeoffs arise. This paper explores them in the context of predicate abstraction.

Subproject(s): S2

Abstract (click to open/close)

Software is ubiquitous in our world and is also becoming prevalent in the realm of missioncritical devices. To prevent lives from being endangered, it is crucial to verify the correctness of such software systems. CSP-OZ-DC is a combination of specification techniques for processes, data, and real-time behavior that admits translation to Phase Event Automata (PEAs) and thereby verification using ARMC, an abstraction-refinement model-checker. Given an undesirable condition, ARMC can prove that the condition will not happen, or it can provide a counterexample trace showing how the condition may occur. Syspect is a modeling application unifying Object-Z, Duration Calculus, and State Machines in a UML (Unified Modeling Language) context. In this work, we integrate ARMC model-checking into Syspect. A lot of information gets lost in the translation process from UML to Transition Constraint Systems, ARMC?s input language. We devise mechanisms and annotations that enable us to nevertheless relate ARMC transitions to high-level specification elements. Our extension smoothly integrates model-checking into the design work-flow, granting the developer a bird?s eye view of how certain faulty states might be reached in a specification.

Subproject(s): R1

Subproject(s): R1

Abstract (click to open/close)

The clause-linking technique of Lee and Plaisted proves the unsatisfiability of a set of first-order clauses by generating a sufficiently large set of instances of these clauses that can be shown to be propositionally unsatisfiable. In recent years, this approach has been refined in several directions, leading to both tableau-based methods, such as the disconnection tableau calculus, and saturation-based methods, such as primal partial instantiation and resolution-based instance generation. We investigate the relationship between these calculi and answer the question to what extent refutation or consistency proofs in one calculus can be simulated in another one.

Subproject(s): H3

Subproject(s): R3

Abstract (click to open/close)

Automata provide a decision procedure for Presburger arithmetic. However, until now only crude lower and upper bounds were known on the sizes of the automata produced by the automata-based approach for Presburger arithmetic. In this paper, we give an upper bound on the number of states of the minimal deterministic automaton for a Presburger arithmetic formula. This bound depends on the length of the formula and the quantifiers occurring in it. We establish the upper bound by comparing the automata for Presburger arithmetic formulas with the formulas produced by a quantifier-elimination method. We show that our bound is tight, also for nondeterministic automata. Moreover, we provide automata constructions for atomic formulas and establish lower bounds for the automata for linear equations and inequations.

Subproject(s): H1

Abstract (click to open/close)

The standard counterexample-guided abstraction-refinement (CEGAR) approach uses finite transition systems as abstractions of concrete systems. We present an approach to represent and refine abstractions of infinite-state systems that uses regular languages instead of finite transition systems. The advantage of using languages over transition systems is that we can store more fine-grained information in the abstraction and thus reduce the number of abstract states. Based on this language-based approach for CEGAR, we present new abstraction-refinement algorithms for hybrid system verification. Moreover, we evaluate our approach by verifying various non-linear hybrid systems.

Subproject(s): H1

Abstract (click to open/close)

Uppaal/DMC is an extension of Uppaal that provides generic heuristics for directed model checking. In this approach, the traversal of the state space is guided by a heuristic function which estimates the distance of a search state to the nearest error state. Our tool combines two recent approaches to design such estimation functions. Both are based on computing an abstraction of the system and using the error distance in this abstraction as the heuristic value. The abstractions, and thus the heuristic functions, are generated fully automatically and do not need any additional user input. Uppaal/DMC needs less time and memory to find shorter error paths than Uppaal's standard search methods.

Subproject(s): R3

Abstract (click to open/close)

Counterexample generation is a crucial task for error diagnosis and debugging of sequential circuits.The simpler a counterexample is - i.e. more general and fewer assigned input values - the better it can be understood by humans. We will use the concept of Black Boxes - parts of the design with unknown behavior - to mask out components for counterexample computation. By this, the resulting counterexample will argue about a reduced number of components in the system in order to facilitate the task of understanding and correcting the error effect.

Subproject(s): S1

Abstract (click to open/close)

We consider the problem of checking whether an incomplete design (i.e. a design containing so-called Black Boxes) can still be extended to a complete design satisfying a given property or whether the property is satisfied for all possible extensions. Motivated by the fact that well-known model checkers like SMV or VIS produce incorrect results for CTL formulas when handling unknowns by using the programs' nondeterministic signals, we present an approximate, yet sound algorithm to process incomplete designs. The algorithm is flexible in the sense that for every Black Box a different method can be chosen. This permits us to handle less relevant Black Boxes (in terms of the CTL formula) with larger approximation and thus faster, whereas we do not lose important information when the possible effect of more relevant Black Boxes is modeled by more exact methods. Additionally, we introduce a concept for exact symbolic model checking of incomplete designs containing several Black Boxes with bounded memory. Finally we give a series of experimental results demonstrating the effectiveness and feasibility of the methods.

Subproject(s): S1

Abstract (click to open/close)

Computing counterexamples is a crucial task for error diagnosis and debugging of sequential systems. If an implementation does not fulfill its specification, counterexamples are used to explain the error effect to the designer. In order to be understood by the designer, counterexamples should be simple, i.e. they should be as general as possible and assign values to a minimal number of input signals. Here we use the concept of Black Boxes -- parts of the design with unknown behavior -- to mask out components for counterexample computation. By doing so, the resulting counterexample will argue about a reduced number of components in the system to facilitate the task of understanding and correcting the error. We introduce the notion of 'uniform counterexamples' to provide an exact formalization of simplified counterexamples arguing only about components which were not masked out. Our computation of counterexamples is based on symbolic methods using AIGs (And-Inverter-Graphs). Experimental results using a VLIW processor as a case study clearly demonstrate our capability of providing simplified counterexamples.

Subproject(s): S1

Abstract (click to open/close)

We provide a framework for fully automated stability verification of piecewise affine systems, both in discrete and continuous time. Starting from the well known linear matrix inequality approach for piecewise quadratic Lyapunov functions, we provide algorithms for the remaining steps needed for full automation. This includes the choice of an adequate state space partitioning into regions and the possible transitions trajectories can take between the regions. To demonstrate the viability of our algorithms, we give examples of systems for which Lyapunov functions can be computed fully automatically.

Keywords: piecewise affine systems, stability verification, linear matrix inequalities
Subproject(s): H4

Abstract (click to open/close)

We show how theorem proving and methods for handling real algebraic constraints can be combined for hybrid system verification. In particular, we highlight the interaction of deductive and algebraic reasoning that is used for handling the joint discrete and continuous behaviour of hybrid systems. We illustrate proof tasks that occur when verifying scenarios with cooperative traffic agents. From the experience with these examples, we analyse proof strategies for dealing with the practical challenges for integrated algebraic and deductive verification of hybrid systems, and we propose an iterative background closure strategy.

Keywords: modular prover combination, analytic tableaux, verification of hybrid systems, dynamic logic
Subproject(s): H3

Abstract (click to open/close)

We introduce a first-order dynamic logic for reasoning about systems with discrete and continuous state transitions, and we present a sequent calculus for this logic. As a uniform model, our logic supports hybrid programs with discrete and differential actions. For handling real arithmetic during proofs, we lift quantifier elimination to dynamic logic. To obtain a modular combination, we use side deductions for verifying interacting dynamics. With this, our logic supports deductive verification of hybrid systems with symbolic parameters and first-order definable flows. Using our calculus, we prove a parametric inductive safety constraint for speed supervision in a train control system.

Keywords: Dynamic logic, sequent calculus, verification of parametric hybrid systems, quantifier elimination
Subproject(s): H3

Abstract (click to open/close)

We introduce a first-order dynamic logic for reasoning about systems with discrete and continuous state transitions, and we present a sequent calculus for this logic. As a uniform model, our logic supports hybrid programs with discrete and differential actions. For handling real arithmetic during proofs, we lift quantifier elimination to dynamic logic. To obtain a modular combination, we use side deductions for verifying interacting dynamics. With this, our logic supports deductive verification of hybrid systems with symbolic parameters and first-order definable flows. Using our calculus, we prove a parametric inductive safety constraint for speed supervision in a train control system.

Keywords: dynamic logic, sequent calculus, verification of parametric hybrid systems, quantifier elimination
Subproject(s): H3

Abstract (click to open/close)

We propose a first-order dynamic logic for reasoning about hybrid systems. As a uniform model for discrete and continuous evolutions in hybrid systems, we introduce hybrid programs with differential actions. Our logic can be used to specify and verify correctness statements about hybrid programs, which are suitable for symbolic processing by calculus rules. Using first-order variables, our logic supports systems with symbolic parameters. With dynamic modalities, it is prepared to handle multiple system components.

Keywords: dynamic logic, hybrid systems, parametric verification
Subproject(s): H3

Abstract (click to open/close)

We combine first-order dynamic logic for reasoning about possible behaviour of hybrid systems with temporal logic for reasoning about the temporal behaviour during their operation. Our logic supports verification of hybrid programs with first-order definable flows and provides a uniform treatment of discrete and continuous evolution. For our combined logic, we generalise the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of dynamic logic. On this basis, we provide a modular verification calculus that reduces correctness of temporal behaviour of hybrid systems to non-temporal reasoning. Using this calculus, we analyse safety invariants in a train control system and symbolically synthesise parametric safety constraints.

Keywords: dynamic logic, sequent calculus, logic for hybrid systems, temporal logic, deductive verification of embedded systems
Subproject(s): H3

Abstract (click to open/close)

We combine first-order dynamic logic for reasoning about possible behaviour of hybrid systems with temporal logic for reasoning about the temporal behaviour during their operation. Our logic supports verification of hybrid programs with first-order definable flows and provides a uniform treatment of discrete and continuous evolution. For our combined logic, we generalise the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of dynamic logic. On this basis, we provide a modular verification calculus that reduces correctness of temporal behaviour of hybrid systems to non-temporal reasoning. Using this calculus, we analyse safety invariants in a train control system and symbolically synthesise parametric safety constraints.

Keywords: dynamic logic, sequent calculus, logic for hybrid systems, temporal logic, deductive verification of embedded systems
Subproject(s): H3

Abstract (click to open/close)

In this paper, we analyze limits of approximation techniques for (non-linear) continuous image computation in model checking hybrid systems. In particular, we show that even a single step of continuous image computation is not semidecidable numerically even for a very restricted class of functions. Moreover, we show that symbolic insight about derivative bounds provides sufficient additional information for approximation refinement model checking. Finally, we prove that purely numerical algorithms can perform continuous image computation with arbitrarily high probability. Using these results, we analyze the prerequisites for a safe operation of the roundabout maneuver in air traffic collision avoidance.

Keywords: model checking, hybrid systems, image computation
Subproject(s): H3

Abstract (click to open/close)

Software model checking with abstraction refinement is emerging as a practical approach to verify industrial software systems. Its distinguishing characteristics lie in the way it applies logical reasoning to deal with abstraction. It is therefore natural to investigate whether and how the use of a constraint-based programming language may lead to an elegant and concise implementation of a practical tool. In this paper we describe the outcome of our investigation. Using a Prolog system together with Constraint Logic Programming extensions as the implementation platform of our choice we have built such a tool, called ARMC (for Abstraction Refinement Model Checking), which has already been used for practical verification.

Subproject(s): R1

Abstract (click to open/close)

We present a method and tool (and implementation) for automatic proofs of region stability for hybrid systems. The formal basis of our approach is the new notion of emph snapshot sequences. We use snapshot sequences for a characterization of region stability. Our abstraction-based algorithm checks the conditions in this characterization. A number of experiments demonstrate the practical potential of our approach.

Subproject(s): H4

Abstract (click to open/close)

Region stability allows one to formalize hybrid systems whose trajectories may oscillate (within a given allowance) even after having `stabilized'. Unfortunately, until today no proof rule (giving necessary and sufficient conditions for the purpose of verifying region stability) has been available. This paper fills the gap. Our (sound and complete) proof rule connects region stability with the finiteness of specific state sequences and thus with the emerging set of verification methods for program termination.

Subproject(s): H4

Abstract (click to open/close)

An acyclic phase-type distribution is a phase-type distribution with a triangular matrix representation. This class of phase-type distribution exhibits special properties and characteristics, which usually result in some ease in analysis. In this paper, we propose a procedure for reducing the size of the state space of any given acyclic phase-type representations.

Subproject(s): S3

Subproject(s): H3

Abstract (click to open/close)

This paper deals with the problem of safety verification of non-linear hybrid systems. We start from a classical method that uses interval arithmetic to check whether trajectories can move over the boundaries in a rectangular grid. We put this method into an abstraction refinement framework and improve it by developing an additional refinement step that employs interval constraint propagation to add information to the abstraction without introducing new grid elements. Moreover, the resulting method allows switching conditions, initial states and unsafe states to be described by complex constraints instead of sets that correspond to grid elements. Nevertheless, the method can be easily implemented since it is based on a well-defined set of constraints, on which one can run any constraint propagation based solver. Tests of such an implementation are promising.

Subproject(s): H1

Abstract (click to open/close)