Abstract (click to open/close)

Technical systems interacting with the real world can be elegantly modelled using probabilistic hybrid automata (PHA). Parametric probabilistic hybrid automata are dynamical systems featuring hybrid discrete-continuous dynamics and parametric probabilistic branching, thereby generalizing PHA by capturing a family of PHA within a single model. Such system models have a broad range of applications, from control systems over network protocols to biological components. We present a novel method to synthesize parameter instances (if such exist) of PHA satisfying a multi-objective bounded horizon specification over expected rewards. Our approach combines three techniques: statistical model checking of model instantiations, a symbolic version of importance sampling to handle the parametric dependence, and SATmodulo- theory solving for finding feasible parameter instances in a multiobjective setting. The method provides statistical guarantees on the synthesized parameter instances. To illustrate the practical feasibility of the approach, we present experiments showing the potential benefit of the scheme compared to a naive parameter exploration approach.

Subproject(s): H1/2,H4

Subproject(s): H1/2

Abstract (click to open/close)

Traffic flow simulation is exploited for estimating the probability that a message --- a hazard warning in this case --- is correctly transmitted to an approaching car in time, that is, before overstepping a safety threshold. The results derived by simulation provide valuable insights in the functional relation between the numerous authoritative parameters and the reliability of timely message reception.

Subproject(s): H1/2

Abstract (click to open/close)

Delay differential equations (DDEs) arise naturally as models of, a.o., networked control systems, where the communication delay in the feedback loop % between controlled system and controller cannot always be ignored. Such delays can e.g.prompt oscillations in otherwise stable feedback loops and thus cause severe deterioration of control performance, invalidating both stability and safety properties. Despite the omnipresence of feedback delays, state-exploratory automatic verification methods have until now concentrated on ordinary differential equations (and their piecewise extensions to hybrid state) only, failing to address the effects of delays on system dynamics. We overcome this problem by iterating bounded degree interval-based Taylor overapproximations of the time-wise segments of the solution to a DDE, thereby identifying and automatically analyzing the operator that yields the parameters of the Taylor overapproximation for the next temporal segment from the current one. By using constraint solving for analyzing the properties of this operator, we obtain a procedure able to provide stability and safety certificates for a simple class of DDEs.

Subproject(s): H1/2,H4

Abstract (click to open/close)

Craig interpolation is widely used in solving reachability and model-checking problems by SAT or SMT techniques, as it permits the computation of invariants as well as discovery of meaningful predicates in CEGAR loops based on predicate abstraction. Extending such algorithms from the qualitative to the quantitative setting of probabilistic models seems desirable. In 2012, [Teige et al.] succeeded to define an adequate notion of generalized, stochastic interpolants and to expose an algorithm for efficiently computing them for stochastic Boolean satisfiability problems, i.e., SSAT. In this work we present a notion of Generalized Craig Interpolant for the stochastic SAT modulo theories framework, i.e., SSMT, and introduce a mechanism to compute such stochastic interpolants for non-polynomial SSMT problems based on a sound and, w.r.t. the arithmetic reasoner, relatively complete resolution calculus. The algorithm computes interpolants in SAT, SMT, SSAT, and SSMT problems. As this extends the scope of SSMT-based model-checking of probabilistic hybrid automata from the bounded to the unbounded case, we demonstrate our interpolation principle on an unbounded probabilistic reachability problem in a probabilistic hybrid automaton.

Subproject(s): H4

Abstract (click to open/close)

This paper presents a transformation-based compositional verification approach for verifying assumption-commitment properties. Our approach improves the verification process by pruning the state space of the model where the assumption is violated. This exclusion is performed by transformation functions which are defined based on a new notion of edges supporting a property. Our approach applies to all computational models where an automaton syntax with locations and edges induces a transition system semantics in a consistent way which is the case for hybrid, timed, Buechi, and finite automata. We have successfully applied our approach to Fischer's protocol.

Subproject(s): H1/2,R1,S2

Abstract (click to open/close)

Determining performance and fault tolerance properties of distributed systems is a challenging task. One common approach to quantify such properties is to construct the state space and the transition model of the distributed system that is to be evaluated. The challenge lies in the state space being exponentially large in the size of the system. One popular approach to tackle this challenge is to combine decomposition and lumping. The system is decomposed, the transition models of the subsystems are constructed and minimized by lumping bisimilar states under an equivalence relation, and the intermediate marginal transition systems are composed to construct the minimal aggregate transition model. The approach allows to circumvent the necessity to construct the full transition model while preserving the ability to compute precise measures. The decomposition yet hinges on the structure of the communication within the system. When processes do not influence each other, decomposition is trivial as it is arbitrary. On the contrary, when all processes are influenced by all other processes --- known as heterarchical structure --- systems cannot be decomposed at all. Between systems of independent and heterarchical processes are i) hierarchically structured systems and ii) systems that are globally hierarchical, but contain locally heterarchical subsystems. The hierarchical type has been addressed previously. This paper targets the second type --- referred to as semi-hierarchically structured ---, thus expanding the frontier from decomposing purely hierarchically structured systems to decomposing semi-hierarchically structured systems. Furthermore, this paper points out the role of different types of execution semantics regarding the decomposition.

Subproject(s): H4

Abstract (click to open/close)

Power grids are parallel systems in which consumers demand a shared resource independent of each other. A blackout occurs when the total demand increases or decreases too rapidly. This paper combines methods and concepts from three domains. The first stems from estimating the power consumption based on thermostatically controlled loads via Markov chains. The second domain provides the composition of parallel systems enriched by intermediate lumping to construct a minimal aggregate transition model, in this case of a community of housings. The third domain provides reasoning about fault tolerance properties by introducing limiting window reliability as measure, suitable to account for the continuous risk of blackouts. Combined, the three methods and concepts allow to determine the risk of blackout of a community over time.

Subproject(s): H4

Abstract (click to open/close)

Set membership estimation (SME) of nonlinear hybrid systems is still a challenging issue. Although SME of nonlinear continuous systems has made significant progress recently, the direct extension of these methods to the hybrid case is not easy. Meanwhile, satisfiability (SAT) checkers for Boolean combinations of arithmetic constraints over real- and integer-valued variables have made significant progress, as they can effectively deal with algebraic constraints between variables and non-linear ODEs, what is denoted as SAT Modulo ODE. Finally, the corresponding solvers solve in a natural way the hybrid differential and algebraic constraints satisfaction problems that underlie SME of hybrid systems. This paper presents the application of such a SAT Modulo ODE solver to SME of hybrid dynamical systems.

Subproject(s): H1/2

Abstract (click to open/close)

Verifying fault tolerance properties of a distributed system can be achieved by state space analysis via Markov chains. Yet, the power of such exact analytic methods is very limited as the state space is exponentially proportional to the system size. We propose a method that alleviates this limit. Lumping is a well known reduction technique that can be applied to a Markov chain to prune redundant information. We propose a system decomposition to employ lumping piecewise on the considerably smaller Markov chains of the subsystems which are much more likely to be tractable. Recomposing the lumped Markov chains of the subsystems results in a configuration space that is likely to be considerably smaller. An example demonstrates how the limiting window availability (i.e. a fault tolerance property) can be computed for a system while exploiting the combination of lumping and decomposition.

Subproject(s): H4

Abstract (click to open/close)

Aiming at automatic verification and analysis techniques for hybrid systems, we present a novel combination of enclosure methods for ordinary differential equations (ODEs) with the iSAT solver for Boolean combinations of arithmetic constraints. Improving on our previous work, the contribution of this paper lies in combining iSAT with VNODE-LP, as a state-of-the-art enclosure method for ODEs, and with bracketing systems which--by exploiting monotonicity properties of the system--allow finding enclosures for problems that VNODE-LP alone cannot enclose tightly. We apply our method to the analysis of a non-linear hybrid system by solving predicative encodings of an inductive stability argument and evaluate the impact of different methods and their interplay in combination.

Subproject(s): H1/2

Abstract (click to open/close)

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

Keywords: measurability, nondeterministic markov process, probabilistic hybrid automaton, reachability, stochastic hybrid automaton
Subproject(s): H4

Abstract (click to open/close)

Symbolic methods in computer-aided verification rely heavily on constraint solvers. The correctness and reliability of these solvers are of vital importance 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. This is in general not the case for unsatisfiability results. 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. Furthermore, we test our approach by enhancing the iSAT constraint solver to generate unsatisfiability proofs, and implemented a tool that can efficiently validate such proofs. Finally, some experimental results showing the effectiveness of our techniques are given.

Subproject(s): H1/2

Abstract (click to open/close)

Specifications and implementations of complex physical systems tend to differ as low level effects such as sampling are often ignored when high level models are created. Thus, the low level models are often not exact refinements of the high level specification. However, they are similar to those. To bridge the gap between those models, we study robust simulation relations for hybrid systems. In this paper, we identify a family of robust simulation relations that allow for certain bounded deviations in the behavior of a system specification and its implementation in both values of the system variables and timings. We show that for this relaxed version of simulation a broad class of logical properties is preserved. The question whether two systems are in simulation relation can be reduced to a reach avoid problem for hybrid games. We provide a sufficient condition under which a winning strategy for these games exists.

Subproject(s): H1/2,H3

Abstract (click to open/close)

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

Subproject(s): H1/2,H4

Abstract (click to open/close)

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

Subproject(s): H1/2,H4

Abstract (click to open/close)

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

Subproject(s): H1/2,H4

Abstract (click to open/close)

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)

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

Subproject(s): R1

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)

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)

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

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)

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)

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)

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)

We present a symbolic algorithm for deciding safety (reachability) of timed systems modelled as Timed Automata (TA), under the notion of robustness w.r.t infinitesimal clock-drift. The algorithm uses a ``neighbourhood'' operator on zones that is efficient to compute. In contrast to other approaches for robustly deciding reachability of TA, which are either region-based (Puri, 2000), (DeWulf, Doyen, Markey, and Raskin, 2004), or involve a combination of forward and backward analyses when zone-based (Daws and Kordy, 2006), ours is a zone-based fully forward algorithm that is guaranteed to terminate, requires no special treatment of cycles in TA, and can be applied to target states that need not be closed.

Subproject(s): H1

Abstract (click to open/close)

In its combination with conflict-driven clause learning the two-watched-literal scheme led to enormous performance gains in propositional SAT solving. The idea of this approach is to accelerate the deduction phase of a SAT solver by saving a high number of unnecessary and expensive computation steps originating in visits of indefinite clauses. In this paper we give a detailed explanation of the generalized watch scheme, called two-watched-atom scheme, implemented in our interval-based constraint solver HySAT, the latter being a solver for mixed Boolean and non-linear arithmetic constraint formulae. As opposed to the purely Boolean setting, the more general form of atomic formulae to be watched in our solver necessitates an extension of the original scheme and calls for a careful design of the data structures employed in the implementation. We present experimental results to demonstrate the speed-up obtained by the proposed scheme.

Subproject(s): H1, H2

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.

Subproject(s): H2

Abstract (click to open/close)

This article presents novel results on automated test generation for hybrid control systems, which involves the generation of both discrete and real-valued, potentially time-continuous, input data to the system under test. Our generation techniques are allocated in two layers: The upper layer contains a symbolic test case generator constructing test cases as paths through an abstracted representation model of the system under test. Different test strategies designed to pursue various quality objectives lead to different selections of symbolic test cases. Symbolic test cases are transformed into feasible, i.e., executable, test cases by constructing concrete sequences of input data, allowing the execution of the pre-planned transition sequence. The input data construction is performed by the lower layer consisting of a constraint solver which applies interval analysis techniques to identify the domains from where to pick the appropriate test data. This process is made efficient by combining subpaving with forward-backward interval constraint propagation. On both layers learning algorithms are applied in order to avoid the spending of computation time on paths and sub-constraints, respectively, which are already known not to contribute to the solution.

Subproject(s): H1,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 extend the paradigm of lazy theorem proving to interval-based arithmetic constraint solving. Algorithmically, our approach deviates substantially from "classical" lazy theorem proving approaches in that it directly controls arithmetic constraint propagation from the SAT solver rather than completely delegating arithmetic decisions to a subordinate solver. From the constraint solving perspective, it extends interval-based constraint solving with all the algorithmic enhancements that were instrumental to the enormous performance gains recently achieved in propositional SAT solving, like conflict-driven learning combined with non-chronological backtracking.

Subproject(s): H1,H2

Abstract (click to open/close)

We present a SAT-based approach to the task and message allocation problem of distributed real-time systems with hierarchical architectures. In contrast to the heuristic approaches usually applied to this problem, our approach is guaranteed to find an optimal allocation for realistic task systems running on complex target architectures. Our method is based on the transformation of such scheduling problems into nonlinear integer optimization problems. The core of the numerical optimization procedure we use to discharge those problems is a solver for arbitrary Boolean combinations of integer constraints. Optimal solutions are obtained by imposing a binary search scheme on top of that solver. Experiments show the applicability of our approach to industrial-size task systems, which are mapped to heterogeneous hierarchical hardware architectures.

Subproject(s): R2,H2

Subproject(s): H1

Abstract (click to open/close)

We transfer the concept of robust interpretation from arithmetic first-order theories to metric-time temporal logics. The idea is that the interpretation of a formula is robust if its truth value does not change under small variation of the constants in the formula. Exemplifying this on Duration Calculus (DC), our findings are that the robust interpretation of DC is equivalent to a multi-valued interpretation that uses the real numbers as semantic domain and assigns Lipschitz-continuous interpretations to all operators of DC. Furthermore, this continuity permits approximation between discrete and dense time, thus allowing exploitation of discrete-time (semi-)decision procedures on dense-time properties.

Keywords: Metric-time temporal logic; Robust interpretation; Discrete time vs. dense time
Subproject(s): H1

Abstract (click to open/close)

We present a SAT-based approach to the task and message allocation problem of distributed real-time systems. In contrast to the heuristic approaches usually applied to this problem, our approach is guaranteed to find an optimal allocation for realistic task systems running on complex target architectures. Our method is based on the transformation of such scheduling problems into nonlinear integer optimization problems. The core of the numerical optimization procedure we use to discharge those problems is a solver for arbitrary Boolean combinations of integer constraints. Optimal solutions are obtained by imposing a binary search scheme on top of that solver. Experiments show the applicability of our approach to industrial-size task systems.

Subproject(s): R2,H2

Subproject(s): H1

Abstract (click to open/close)

We present a concept to significantly advance the state of the art for bounded model checking (BMC) and inductive verification (IV) of hybrid discrete-continuous systems. Our approach combines the expertise of partners coming from different domains, like hybrid systems modeling and digital circuit verification, bounded planning and heuristic search, combinatorial optimization and integer programming. After sketching the overall verification flow we present first results indicating that the combination and tight integration of different verification engines is a first step to pave the way to fully automated BMC and IV of medium to large-scale networks of hybrid automata.

Keywords: Hybrid System Verification, Bounded Model Checking, Inductive Verification, Verification Engines
Subproject(s): H2

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