ARCH17: Papers with Abstracts

Abstract. Autonomy holds a great promise by improving the applications, safety, and efficiency of flight. If little operator input is necessary, unmanned rotorcraft have a wide range of applications ranging from cargo delivery to inspection. Currently unmanned rotorcraft are underutilized because they either have to fly on preplanned missions at high altitude or require careful teleoperation. A capable autonomous rotorcraft will have to react quickly to previously unknown obstacles, land at unprepared sites, and fly with semantic information to enable long-term autonomy in cluttered environments.
In this talk we give an overview of how autonomy systems are currently designed and how pushing the performance and safety of these systems challenges current verification paradigms. In particular we will address how a supervisory layer in the motion planning system can improve safety, a sensor steering system enables us to optimize coverage for safe trajectories, and how semantic information can help us guide the rotorcraft.

Abstract. In this paper we describe an energy management benchmark problem for a smart grid where electrical energy is supplied to a load via local power production from a solar PhotoVoltaic (PV) installation. The smart grid is connected with the main grid, which can eventually provide the energy needed for balancing demand and generation. The goal is to set the battery energy flow so as to keep the energy exchange with the main grid as close as possible to a nominal profile, within certified bounds, avoiding the fluctuations caused by the local PV energy production. Some energy production profiles of the PV installation and environmental data on irradiation and temperature are available for the design of the energy management strategy, together with a hybrid model for the battery and the electrical load profile. We describe a data-driven solution, pointing out its limits and providing some hint on possible direction for improvement.

Abstract. A fundamental maneuver in autonomous space operations is known as rendezvous, where a spacecraft navigates to and approaches another spacecraft. In this case study, we present linear and nonlinear benchmark models of an active chaser spacecraft performing rendezvous toward a passive, orbiting target. The system is modeled as a hybrid automaton, where the chaser must adhere to different sets of constraints in each discrete mode. A switched LQR controller is designed accordingly to meet this collection of physical and geometric safety constraints, while maintaining liveness in navigating toward the target spacecraft. We extend this benchmark problem to check for passive safety, which is collision avoidance along a passive, propulsion-free trajectory that may be followed in the event of system failures. We show that existing hybrid verification tools like SpaceEx, C2E2, and our own implementation of a simulation-driven verification tool can robustly verify this system with respect to the requirements, and a variety of relevant initial conditions.

Abstract. This benchmark suite consists of a number of examples of autonomous multi-agent systems where the agent number ranges from two to ten. The benchmarks are derived from the field of position-based formation control in autonomous robotics and vehicles. Their models are given as network of hybrid automata in the SpaceEx XML model format and can be transformed to other verification tools model formats using HyST, a model trans- formation tool. Safety of a small benchmark with two agents is analyzed using SpaceEx.

Abstract. This benchmark presents an implementation of a standard control stack for an Autonomous Vehicle (AV). The control stack is made up of a behavioral planner (providing waypoints for the AV to visit in sequence), a trajectory planner (which computes smooth trajectory that the AV should follow to go between waypoints) and a trajectory tracker (which actuates the AV to make it follow the planned trajectory as closely as possible). The behavioral planner is purposefully simple, while the trajectory planner is a a high-fidelity approximation of a planner that was tested on a real Prius, and the tracker was validated by others in previous work on a real Cadillac SRX. The interest of this benchmark is that it includes all three components, rather than one AV control subsystem (such as only adaptive cruise control or only a lane-keeper), and the planners are significantly more realistic than most existing benchmarks or models. It can be used as a baseline AV system for verification and testing tools, which must be able to handle at least the complexity of this controller. This includes simple choices made by the behavioral planner when the current waypoint cannot be reached, discrete and continuous nonlinear optimizations solved by the trajectory planner, and nonlinear ODEs solved by the trajectory tracker. The bench- mark comes with three road topologies: a free space with obstacles, a curved road, and a roundabout.

Abstract. Various mission-critical applications necessarily require a transformer in switching converters to obtain DC isolation between the converters’ input and output. Since DC-DC converters are the switching devices, these are modeled as hybrid automata. We present hybrid automaton modeling of two main types of transformer isolated DC-DC converters, namely, flyback and forward converters. We have also catered the non-determinism for both. We use HyST (Hybrid Source Transformation) tool to automatically generate the models in SpaceEx format, perform reachability analysis, and then automatically convert the models into Mathworks Simulink Stateflow (SLSF) using HyST. Thus we demonstrate effectiveness of HyST tool in the model-based design process. The HyST user needs not to manually construct or modify the models thus saving significant amount of time and efforts.

Abstract. At scale, formal verification of hybrid systems is challenging, but a potential remedy is the observation that systems often come with a number of natural components with certain local responsibilities. Ideally, such a compartmentalization into more manageable components also translates to hybrid systems verification, so that safety properties about the whole system can be derived from local verification results. We propose a benchmark consisting of a sequence of three case studies, where components interact to achieve system safety. The baseline for the benchmark is the verification effort from a monolithic fashion (i.e., the entire system without splitting it into components). We describe how to split the system models used in these case studies into components with local responsibilities, and what is expected about their interaction to guarantee system safety. The benchmark can be used to assess the performance, automation, and verification features of component-based verification approaches.

Abstract. The artificial pancreas concept automates the delivery of insulin to patients with type-1 diabetes, sensing the blood glucose levels through a continuous glucose monitor (CGM) and using an insulin infusion pump to deliver insulin. Formally verifying control algorithms against physiological models of the patient is an important challenge. In this paper, we present a case study of a simple hybrid multi-basal control system that switches to different preset insulin delivery rates over various ranges of blood glucose levels. We use the Dalla- Man model for modeling the physiology of the patient and a hybrid automaton model of the controller. First, we reduce the problem state space and replace nonpolynomial terms by approximations with very small errors in order to simplify the model. Nevertheless, the model still remains nonlinear with up to 9 state variables.
Reachability analysis on this hybrid model is used to verify that the blood glucose levels remain within a safe range overnight. This poses challenges, including (a) the model exhibits many discrete jumps in a relatively small time interval, and (b) the entire time horizon corresponding to a full night is 720 minutes, wherein the controller time period is 5 minutes. To overcome these difficulties, we propose methods to effectively handle time- triggered jumps and merge flowpipes over the same time interval. The evaluation shows that the performance can be improved with the new techniques.

Abstract. Cyber-physical production systems (CPPS) build a network of industrial automation components and systems to enable individualized products at mass production costs. Failures or vulnerabilities in CPPS can be life threatening and can cause physical damage while hiding the effects from monitors. Thus, software verification and validation methods need to analyze the dynamics and behavior of CPPS. In this work, we present a hybrid testbed used in Siemens Corporate Technology. The testbed combines a physical CPPS together with its virtual simulated counterpart, allowing us to verify the system using runtime monitoring, model-based testing, simulation and formal techniques.

Abstract. The wind turbine benchmark is part of the ARCH benchmark repository. It entails closed- loop requirements and encompasses nonlinear and hybrid dynamics. Owing its origin to industry based applications, the benchmark modeling is done with MATLAB/Simulink. Formal verification tools, however, do not operate on simulation models but on formal models, such as hybrid automata. Particularly efficient verification algorithms are known for systems with Piecewise Affine (PWA) dynamics. In this vein, we construct a PWA model of the wind turbine in the SX format, which formally describes a network of hy- brid automata and can be used by several reachability tools. The model transformation follows a four-step approach with the aim of (i) adapting the Simulink model to obtain a verification model (ii) translating the Simulink blocks to equivalent blocks in SX format, (iii) conducting compositional, syntactic hybridization to obtain a PWA approximation of the dynamics of the nonlinear blocks, and (iv) performing model validation. We also report some preliminary experiments on the subsystems (network components) of the wind turbine that we conducted with SpaceEx.

Abstract. We evaluate a recently-proposed reachability method on a set of high-dimensional lin- ear system benchmarks taken from model order reduction and presented in ARCH 2016. The approach uses a state-set representation called a generalized star set and the principle of superposition of linear systems to achieve scalability. The method was previously shown to have promise in terms of scalability for direct analysis of large linear systems. For each benchmark, we also compare computing the basis matrix, a core part of the reachabil- ity method, using numerical simulations versus a matrix exponential formulation. The approach successfully analyzes systems with hundreds of dimensions in minutes, and can scale to systems that have over 10000 dimensions with a computation time ranging from tens of minutes to tens of hours, depending on the desired time step.

Abstract. This report presents results of a friendly competition for formal verification of continuous and hybrid systems with piecewise constant dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, four tools have been applied to solve five different benchmark problems in the category for piecewise constant dynamics: BACH, Lyse, PHAVer, and VeriSiMPL. The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with piecewise constant dynamics up to this date.

Abstract. This report presents results of a friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, three tools have been applied to solve three different benchmark problems in the category ofbounded model checking of hybrid systems with piecewise constant dynamics (in alphabetical order): BACH, HyDRA, and XSpeed. The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools and we also welcome more tools to join in this friendly competition in the future event.

Abstract. This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, seven tools have been applied to solve three different benchmark problems in the category for linear continuous dynamics (in alphabetical order): Axelerator, CORA, Flow*, HyDRA, Hylaa, SpaceEx, and XSpeed. The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with linear continuous dynamics up to this date.

Abstract. We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. This year, three tools CORA, Flow* and Isabelle/HOL (in alphabetic order) participated. They are applied to solve the reachability analysis problems on three benchmarks which have 2, 7 and 12 variables respectively. We do not rank the tools based on the results, but show the current status and discover the potential advantages of different tools. Besides, the computational settings presented here provide a guide to use the tools although they might not be optimal.

Abstract. This report presents some preliminary base results from the 2017 friendly competition in the ARCH workshop for the falsification of temporal logic specifications over Cyber-Physical Systems. The benchmarks are available on the ARCH website. In this report, we present results on a powertrain model developed by Toyota Technical Center which contains a complex automatic air-fuel control subsystem

Abstract. This report presents the results of the repeatability evaluation for a friendly competition for formal verification of continuous and hybrid systems. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, thirteen tools have been applied to solve benchmark problems for the six competition categories, of which, ten tools were evaluated and passed the repeatability evaluation. The repeatability results represent a snapshot of the current landscape of tools and the types of benchmarks for which they are particularly suited and for which others may repeat their analyses. Due to the diversity of problems in verification of continuous and hybrid systems, as well as basing on standard practice in repeatability evaluations, we evaluate the tools with pass and/or failing being repeatable. These re- sults probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems up to this date.