ARCH16:Papers with AbstractsPapers 

Abstract. Implantable cardiac devices like pacemakers and defibrillators are lifesaving 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 nbyn 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. Analogmixed signal (AMS) circuits are widely used in various missioncritical applications necessitating their formal verification prior to implementation. We consider modeling two AMS circuits as hybrid automata, particularly a charge pump phaselocked loop (CPPLL) and a fullwave 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 VHDLAMS description of a circuit based on the verified model.  Abstract. In this paper we propose a benchmark for verification of properties of faulttolerant 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 nonfaulty 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 righthand sides, or systems of affine ODEs. More recently, verification tools capable of working with nonlinear differential equations have been developed. The behavior of nonlinear systems is known to be in general extremely difficult to analyze because solutions are rarely available in closedform. In order to assess the practical utility of the various verification tools working with nonlinear 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 nonlinear 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 realtime 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 smallscale. 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 largescale 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 modelorder reduction algorithms in control and numerical analysis. Each example is provided in the SpaceEx XML model format as singlemode 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 MATLABbased 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, plugins 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 highlevel 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 highlevel analysis method is counterexample guided abstraction refinement (CEGAR), where, at each iteration, the model is refined based on the counterexample produced by the reachability computation.
In this paper, we present hypy, a python library which strives to ease the development of highlevel analysis approaches. Hypy provides the necessary machinery to run a number of uptodate hybrid systems analysis tools, parse their outputs, and modify the models. The modifications are performed using HyST, a sourcetosource 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 nonCEGAR case studies: abstraction for parameter identification, generation of pseudoinvariants 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 proofofconcept tool formalSpec for semiautomatic 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 CyberPhysical 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. CounterexampleGuided 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 proofofconcept tool, optimizations, and first experiments.  Abstract. We propose a computational approach to approximate the value function and control policies for a finite horizon stochastic reachavoid problem as follows. First, we formulate an infinite dimensional linear program whose solution characterizes the optimal value function of the stochastic reachavoid. Next, we introduce sumofsquares 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. 

