Abstract. Hypnosis, or depth of unconsciousness, is one of the goals of general anesthesia. In this brief paper we provide a differential equation model of how propofol, a commonly used intravenous anesthetic drug, leads to hypnosis. The model has two components: the pharmacokinetics (PK) describing how the drug is metabolized by the body, and the pharmacodynamics (PD) describing how the drug effects the depth of hypnosis. This standard PK/PD model is a compartmental model, and is linear except for an internal time delay and a nonlinear output mapping. We discuss how this model can be simplified and/or complexified so as to take best advantage of the capabilities of a particular analysis method. One goal of developing such a model is to ensure patient safety during surgery, so we describe an example safety verification problem. Finally, in order to demonstrate that this benchmark is operational, we provide code to simulate one version of the system. |
Abstract. This paper introduces the Motor-Transmission Drive System as a benchmark example for the safety analysis of hybrid systems.
In particular, we illustrate the problem of checking the gear meshing duration and the impact impulse (both of which we refer to as safety) of the Motor-Transmission Drive System.
We aim to provide a complete problem description to which different verification tools or approaches for safety analysis can be applied and compared.
For this reason, we first elaborate on a hybrid automaton (HA) model of the Motor-Transmission Drive System to describe the gear meshing process with uncertain initial states, and then we specify the safety property of interest.
Next, we clarify the characteristic phenomena exhibited by the benchmark which make the verification problem hard to solve.
Finally, we show some simulation results to illustrate the influences of the initial states on the safety property.
This benchmark example can help the researchers and engineers to find appropriate methods for safety verification of this kind of hybrid system. |
Abstract. Power electronics represent a large and important class of hybrid systems, as modern digital computers and many other systems rely on their correct operation. In this benchmark description, we model three DC-to-DC switched-mode power converters as hybrid automata with continuous dynamics specified by linear ordinary differential equations. A DC-to-DC converter transforms a DC source voltage from one voltage level to another utilizing switches toggled at some (typically kilohertz) frequency with some duty cycle. The state of this switch gives rise to the locations of the hybrid automaton, and the continuous variables are currents and voltages. The main contributions of this benchmark description include: (a) unified modeling of three types of converters as a hybrid automaton with two locations and differing continuous dynamics, and (b) a basic benchmark generator that allows for simulation of these converters in Simulink/Stateflow and reachability analysis in SpaceEx. Future challenges for these benchmark classes include closed-loop control, where the speeds of plant and controller dynamics differ by orders of magnitude. |
Abstract. We propose to standardize two Matlab/Simulink models of automotive systems as benchmark problems for hybrid system verification. Both
models can be simulated quickly, making them ideal for testing-based verification methods that require a significant number of system output trajectories. One of the benchmarks is the Automatic Transmission model, which is deterministic. The other benchmark is the Fault-Tolerant Fuel Control System, which exhibits stochastic behavior. Our benchmark standardization defines a number of Metric Temporal Logic requirements that must be satisfied by the models. |
Abstract. The benchmark presented in this paper is an example for verification of a hybrid system model with so-called holes, i.e. part of the system behaviour is not specified. Verification of such a model allows 3rd parties to plug a specific behaviour into a hole without changing desirable properties of the system. The particular example is based on an open-source robotics application, namely a self-balancing two-wheeled robot which is essentially modeled as an inverted pendulum. The balance controller provides two input signals for translational (forward/backward) and rotational (left/right turn) motion which can be driven by arbitrary path planning applications. Examples for such applications are line following and pursuit-evasion algorithms as well as a remote control which allows trajectories to be defined externally. These motion trajectories may or may not yield a state from which the balance controller is unable to recover, which means that the robot falls over. Hence, the verification goal is to prove the safety property that the body pitch angle is bounded under motion trajectories. |
Abstract. A practical benchmark for testing analysis and verification methods for continuous as well as hybrid systems is suggested. It consists of a platoon of controlled vehicles. The vehicles exchange information via a communication network that is subject to failure of single nodes or a complete loss of communication. The worst case scenario corresponding to the transition from a fully functioning communication between the vehicles to a total loss of communication is considered in particular. The safety properties of the considered networked platoon are investigated. The system is modeled as a hybrid automaton. The continuous part represents the dynamical behavior of the platoon and the
discrete part are spontaneous events related to the switching communication topology. The proposed example is a linear time invariant system. |
Abstract. This paper proposes a simplified hybrid model of a freight train equipped with an air brake. The control of such a system and the enforcement of numerous safety constraints constitute a relevant benchmark to evaluate tools for proving safety requirements in hybrid systems. |
Abstract. In this experience report, we apply the hybrid verification tools
iSAT-ODE, Flow*, and S-TaLiRo to a case study consisting of an experimental
electro-mechanical braking system. Starting from a Simulink closed-loop
model, we describe the derivation of hybrid automaton models for plant
and controller and give verifcation results for the different tools. |
Abstract. We present a case study of attitude control for a quadrotor and propose the application of reachability analysis to enhance the robustness of the control design.
The controller is to be implemented and tested using an experimental nano-quadrotor platform, the \emph{CrazyFlie}.
We intend to use measured data to improve the models employed in the reachability analysis and, therefore, enhance the reliability of the controller design. |
Abstract. We present a new model of a tank network used to transfer liquid. Tanks are connected by channels. The throughput velocity of every particular channel is governed by the controller. We consider a special class of stratified controllers which are organized in several phases. Every phase can be further partitioned into multiple options. This structure makes it easy to generate a variety of benchmark instances ranging in the size, branching factor and generally analysis complexity. We provide a flexible benchmark generator for this class of benchmarks and a sample benchmark suite built by the generator. Finally, we use the Hyst model transformation framework to convert the original model in a format compatible with several reachability tools. |
Abstract. While requirements engineering has received considerable attention in
academia over the past years, formalization of requirements for physically
influenced systems is still a difficult task in practice. In this paper, we give
formal representations of some typical requirement classes arising in the
automotive industry. We divide these patterns into three main classes:
those mostly referring to properties of continuous signals, those mostly
referring to discrete events and those referring to similarity to a reference
signal. We discuss these patterns on concrete examples from automotive
embedded systems, where specifications are used for test case generation. |
Abstract. The field of numerical analysis has developed numerous benchmarks for evaluating differential and algebraic equation solvers. In this paper, we describe a set of benchmarks commonly used in numerical analysis that may also be effective for evaluating continuous and hybrid systems reachability and verification methods. Many of these examples are challenging and have highly nonlinear differential equations and upwards of tens of dimensions (state variables). Additionally, many examples in numerical analysis are originally encoded as differential algebraic equations (DAEs) with index greater than one or as implicit differential equations (IDEs), which are challenging to model as hybrid automata. We present executable models for ten benchmarks from a test set for initial value problems (IVPs) in the SpaceEx format (allowing for nonlinear equations instead of restricting to affine) and illustrate their conversion to several other formats (dReach, Flow*, and the MathWorks Simulink/Stateflow [SLSF]) using the HyST tool. For some instances, we present successful analysis results using dReach and SLSF. |
Abstract. We present approximate PWA models of a powertrain control benchmark. |
Abstract. In Model Based Development (MBD) of embedded systems, it is often desirable to verify or falsify certain formal specifications. In some cases it is also desirable to find the range of specification parameters for which the specification does not hold on the system. We illustrate these methods on a challenge problem from the automotive industry on a high-fidelity, industrial scale engine model. |
Abstract. The philosophy, architecture, and capabilities of the COntinuous Reachability Analyzer (CORA) are presented. CORA is a toolbox that integrates various vector and matrix set representations and operations on them as well as reachability algorithms of various dynamic system classes. The software is designed such that set representations can be exchanged without having to modify the code for reachability analysis. CORA has a modular design, making it possible to use the capabilities of the various set representations for other purposes besides reachability analysis. The toolbox is designed using the object oriented paradigm, such that users can safely use methods without concerning themselves with detailed information hidden inside the object. Since the toolbox is written in MATLAB, the installation and use is platform independent. |
Abstract. This paper gives a brief overview of the new features introduced in the latest version of the tool Flow*. We mainly describe the new efficient scheme for integrating linear ODEs. We show that it can efficiently handle the challenging benchmarks on which, to the best of our knowledge, only SpaceEx works. Moreover, it is also possible to extend the method to deal with unbounded initial sets. A comparison between Flow* 1.2 and SpaceEx on those benchmarks is given. Besides, we also investigate the scalability Flow* 1.2 based on our non-linear line circuit benchmarks. |
Abstract. We present BluSTL, a MATLAB toolbox for generating controllers from
specifications written in Signal Temporal Logic (STL). The toolbox takes as input a system and a
set of constraints expressed in STL and constructs an open-loop or a closed-loop (in a receding
horizon or Model Predictive fashion) controller that enforces these constraints on the system
while minimizing some cost function. The controller can also be made reactive or robust to some
external input or disturbances. |
Abstract. The problem of conceiving a controller for networked systems is a challenging task
because of the complex interaction of its different components with each other and also with the environment around them. The design process becomes more difficult if large-scaled systems are involved. We propose reachability analysis of continuous systems to guarantee control requirements which because of the complexity of the problem could not be taken into account during the control design. As example we suggest a large-scalable platoon of trucks. We use our own support function implementation to assess the performances of the obtained controlled
platoon and then decide about the best performing controller. |
Abstract. We present a tool for reachability analysis of continuous systems based on
affine arithmetic and Runge-Kutta methods. The distinctive feature of our tool
is its verification in the interactive theorem prover Isabelle/HOL: the
algorithm is guaranteed to compute safe overapproximations, taking into account
all round-off and discretization errors. |
Abstract. Analysis problems of hybrid systems, involving nonlinear real functions and ordinary differential equations, can be reduced to SMT (satisfiability modulo theories) problems over the real numbers. The dReal solver can automatically check the satisfiability of such SMT formulas up to a given precision δ > 0. This paper explains how bounded model checking problems of hybrid systems are encoded in dReal. In particular, a novel SMT syntax of dReal enables to effectively represent networks of hybrid systems in a modular way. We illustrate SMT encoding in dReal with simple nonlinear hybrid systems. |
Abstract. In this paper, we present experimental results from running
SpaceEx on some of the benchmarks of the ARCH14 workshop. Some of
the SpaceEx models were obtained from Matlab/Simulink models with
the help of a new translation tool. While some benchmarks could be
handled to our satisfaction, several still pose signicant challenges. We
discuss possible alternatives for handling the problematic cases. |
Abstract. In this paper, we present the progress we have made in verifying the benchmark powertrain control systems introduced in the last ARCH workshop. We implemented the algorithm for computing local discrepancy (rate of convergence or divergence of trajectories) reported in the hybrid system verification tool C2E2. We created Stateflow translations of the original models to aid the processing using C2E2 tool. We also had to encode the different driver behaviors in the form of state machines. With these customizations, we have been successful in verifying one of the easier (but still challenging) benchmarks from the powertrain suite. In this paper, we present some of the engineering challenges and describe the artifacts we created in the process. |
