ARCH16: Papers with Abstracts

Abstract. Implantable cardiac devices like pacemakers and defibrillators are life-saving medical devices.
To verify their functionality, there is a need for heart models that can simulate interesting phenomena and are relatively computationally tractable.
In this benchmark we implement a model of the electrical activity in excitable cardiac tissue as a network of nonlinear hybrid automata.
The model has previously been shown to simulate fast arrhythmias.
The hybrid automata are arranged in a square n-by-n grid and communicate via their voltages.
Our Matlab implementation allows the user to specify any size of model n, thus rendering it ideal for benchmarking purposes since we can study tool efficiency as a function of size.
We expect the model to be used to analyze parameter ranges and network connectivity that lead to dangerous heart conditions.
It can also be connected to device models for device verification.

Abstract. A cardiac model of networked Hybrid Automata (HA) cells or nodes is potentially very useful for industry validation of pacemaker algorithms. Such a model replicates the electrical conduction system of the heart and the interaction with a pacemaker. The benchmark is a network of more than 100 HAs. It exhibits several key phenomena that are typical for hybrid systems and reachability analysis.

Abstract. This paper proposes a simplified nonlinear model of a wind turbine equipped with a switching controller. The composition of wind turbine and controller results in a hybrid system. The control of such a system and the enforcement of numerous safety and performance constraints constitute a relevant benchmark to evaluate tools for proving safety requirements in hybrid systems.

Abstract. Analog-mixed signal (AMS) circuits are widely used in various mission-critical applications necessitating their formal verification prior to implementation. We consider modeling two AMS circuits as hybrid automata, particularly a charge pump phase-locked loop (CP-PLL) and a full-wave rectifier (FWR). We present executable models for the benchmarks in SpaceEx format, perform reachability analysis, and demonstrate their automatic conversion to MathWorks Simulink/Stateflow (SLSF) format using the HyST tool. Moreover, as a next step towards implementation, we present the VHDL-AMS description of a circuit based on the verified model.

Abstract. In this paper we propose a benchmark for verification of properties of fault-tolerant
clock synchronization algorithms, namely, a benchmark of a TTEthernet network, where
properties of the clock synchronization algorithm as implemented in a TTEthernet network can be verified, and optimization techniques for verification purposes can be applied.
Our benchmark, which assumes non-faulty components, aims to be a basis for verifying
configurations which include faulty components, information consistency mechanisms, and for verifying other clock synchronization algorithms.

Abstract. Safety verification of hybrid dynamical systems relies crucially on the ability to reason about reachable sets of continuous systems whose evolution is governed by a system of ordinary differential equations (ODEs). Verification tools are often restricted to handling a particular class of continuous systems, such as e.g. differential equations with constant right-hand sides, or systems of affine ODEs. More recently, verification tools capable of working with non-linear differential equations have been developed. The behavior of non-linear systems is known to be in general extremely difficult to analyze because solutions are rarely available in closed-form. In order to assess the practical utility of the various verification tools working with non-linear ODEs it is very useful to maintain a set of verification problems. Similar efforts have been successful in other communities, such as automated theorem proving, SAT solving and numerical analysis, and have accelerated improvements in the tools and their underlying algorithms. We present a set of 65 safety verification problems featuring non-linear polynomial ODEs and for which we have proofs of safety. We discuss the various issues associated with benchmarking the currently available verification tools using these problems.

Abstract. Formal methods refers broadly to techniques for the verification and
automatic synthesis of transition systems that satisfy desirable properties
exactly or within some statistical tolerance. Though historically developed for
concurrent software, recent work has brought these methods to bear on motion
planning in robotics. Challenges specific to robotics, such as uncertainty and
real-time constraints, have motivated extensions to existing methods and
entirely novel treatments. However, compared to other areas within robotics
research, demonstrations of formal methods have been surprisingly small-scale.
The proposed benchmark seeks to motivate advancement of the state of
the art toward practical realization by testing scalability of existing tools, and
motivating improvements.

Abstract. This benchmark suite is composed of nine examples of large-scale linear systems, ranging in dimensionality in the tens to the low thousands. The benchmarks are derived from diverse fields such as civil engineering and robotics, and are based on similar existing test sets for model-order reduction algorithms in control and numerical analysis. Each example is provided in the SpaceEx XML model format as single-mode hybrid automaton and are compatible with the HyST model transformation tool to support analysis in other verification tools. Some preliminary reachability analysis results for some of the smaller examples (on the order of tens of dimensions) are presented using SpaceEx.

Abstract. We present HyReach, a MATLAB-based toolbox for reachability
analysis of linear hybrid systems based on support functions. The
main goal of HyReach is to provide a single graphical user interface for
easily configurable reachability analysis on different systems. HyReach
offers a number of known algorithms for the computation of reachable
sets within modes. These are combined with various approaches of handling
mode invariants, guard intersection computations and transition
strategies. Furthermore, plug-ins like the MPT and CVX toolboxes complement
the existing MATLAB optimization toolbox to increase the variety
of optimization algorithms for the computation of support functions.
HyReach supports both textual and graphical inputs and outputs, allowing
for flexibility and seamlessness in workflow and processing of data.
We illustrate these features with examples in this paper.

Abstract. Hybrid systems play an important role in many application domains. A range of powerful analysis methods for this class of systems perform high-level analysis, where, iteratively, (1) a reachability computation is performed on a system model, (2) the result of the analysis is examined, and (3) the model is modified and the process repeats. For example, a well- known high-level analysis method is counter-example guided abstraction refinement (CEGAR), where, at each iteration, the model is refined based on the counter-example produced by the reachability computation.

In this paper, we present hypy, a python library which strives to ease the development of high-level analysis approaches. Hypy provides the necessary machinery to run a number of up-to-date hybrid systems analysis tools, parse their outputs, and modify the models. The modifications are performed using HyST, a source-to-source model transformation framework, which supports output formats including SpaceEx, Flow*, dReach, and HyCreate. HyST, however, does not run reachability tools nor interpret their output. The developed hypy library fills this gap, providing an extendable and flexible architecture which simplifies development of complex analysis strategies. We demonstrate its practical potential on three non-CEGAR case studies: abstraction for parameter identification, generation of pseudo-invariants to reduce reachability overapproximation error, and completely automatic tool parameter tuning for the Flow* reachability tool.

Abstract. Interval arithmetic can be seen as one of the workhorses for formal verification approaches. The popularity of interval arithmetic stems form the fact that the possible outcomes of almost all frequently occurring mathematical expressions can be bounded. A disadvantage of interval arithmetic is that due to the negligence of dependencies of variables in expressions, results can be overly conservative. For this reason, interval arithmetic is typically used in formal verification tools when formulas are not contributing much to the accuracy of the overall approach, but do not belong to a restrictive class of expressions and are thus hard to evaluate. Although a lot of textbooks and software manuals for interval arithmetic exist, we have not found a complete and detailed description of how all standard mathematical functions are evaluated. This work changes this situation and describes concisely the evaluation of all standard mathematical functions. The described techniques are implemented as a class in CORA, a free MATLAB tool for continuous reachability analysis. Previously, CORA used the MATLAB toolbox INTLAB, but this tool is no longer freely available. Thus, our interval arithmetic class is currently the only freely available implementation of interval arithmetic that runs under current MATLAB versions. We have thoroughly tested our implementation against INTLAB and present the results.

Abstract. We present the proof-of-concept tool formalSpec for semi-automatic translation of system requirements from controlled natural language into hybrid automata. These can be automatically integrated as monitor automata with an existing SpaceEx system model.

Abstract. We describe practical experiences on verifying a steering
controller specification. The hybrid automaton implements a PI control rule and
considers the vehicle's velocity as input from the environment. By combining
the tools Stabhyli and SoapBox, we establish several safety and liveness
properties for the steering controller, including convergence towards an
equilibrium.

Abstract. We present a simple, yet flexible parameter synthesis and repair approach for Cyber-Physical Systems (CPS). The user defines the behavior of a CPS, a set of (un)safe states, and a generic template for an inductive invariant using Satisfiability Modulo Theories (SMT) formulas. Counterexample-Guided Inductive Synthesis (CEGIS) is then used to compute values for open parameters and a concrete invariant to prove that all unsafe states are unreachable. Using templates for expressions, the approach can also be used for CPS repair. We present a proof-of-concept tool, optimizations, and first experiments.

Abstract. We propose a computational approach to approximate the value function and control policies for a finite horizon stochastic reach-avoid problem as follows. First, we formulate an infinite dimensional linear program whose solution characterizes the optimal value function of the stochastic reach-avoid. Next, we introduce sum-of-squares polynomials to approximate the solution of this linear program through a semidefinite program. We compare our proposed tool to alternative numerical approaches via several case studies.