In the Ford-RWTH Research Alliance project “Safety Verification for Mixed Discrete-Continuous Automotive Systems”, Ford Motor Company and RWTH Aachen University joined their forces to analyze the capabilities of discrete-continuous (hybrid) systems analysis tools and their potential employment in the automotive sector. We are grateful to Ford Motor Company for funding and continuously supporting our activities throughout the whole project phase.
To experiment with different tools implementing different methodologies for the analysis of discrete-continuous systems, we collected several publicly available benchmarks and converted them to the input languages of some of the available tools. On this page we make these model specifications publicly available to support the research community and interested users. This data should also allow to repeat our experiments and verify our observations, which we collected in a submission to the International Journal on Software Tools for Technology Transfer.
In the following we give a short description of six applications (benchmark families), from which we considered 14 concrete problems (benchmarks instances).
Building (linear, continuous): The building benchmark (bld_48) has been proposed to the ARCH benchmark collection as a large-scale, continuous system [1]. It considers a simplified model of the Los Angeles Hospital, a building with eight storeys modeled by a continuous system comprised of 48 variables. The displacement and dynamics of each storey is modeled by a beam-model.
The goal is to validate, whether an initial displacement converges to a stable equilibrium within reasonable time and with limited over-shoot. In the instance considered, the displacement modelled by variable x25 should never exceed a bound of 0.006 within the first 20 time units (time horizon). This benchmark is a constant part of the ARCH Friendly Competition.
Vehicle Platoon (linear, hybrid): We consider two instances (plt_30 and plt_42) of the vehicle platoon benchmark [2]. This benchmark is one of the first benchmarks proposed to ARCH and has been used in various evaluations, amongst them it has been a constant part of the ARCH Friendly Competition. The system models a platoon of three vehicles, where the first one is human-driven and the two following ones are autonomous. The vehicle distance, speed and acceleration are modeled via 9 state variables. The following vehicles are equipped with a controller to keep the distance at a certain level. In the model, the vehicles communicate the current distances via radio; the model contains a location for normal operation of the radio and a second location representing disturbed communication in which the dynamics changes as the controller does not get proper input readings. While in the original version of the benchmark communication breakdowns could happen at arbitrary points in time, simplified versions have been used in the ARCH Friendly Competition where the communication breaks down deterministically as most tools cannot handle arbitrary switching.
The safe region in the two models bounds the distance between the vehicles to at least 30 m respectively 42 m. The time horizon is set to 20 time units, due to the deterministic switching every 5 time units at most 3 discrete jumps are analyzed.
Filtered Oscillator (linear, hybrid): Being designed as a scalable model, the filtered oscillator benchmark comes with four instances (flt_04, flt_08, flt_16 and flt_32). This model has been presented in the context of the publication of the tool SpaceEx as one of the benchmarks [3] and been re-used in later publications to show performance improvements. The system consists of a switched oscillator system modeled via four locations, where the output of the oscillator is smoothed by a series of first-order filters. In this work, the number next to each instance denotes the number of applied filters. The state space is built from two variables which are used to model the oscillator and additional k variables for a series of k filters.
The specification aims at keeping one of the variables y used to describe the oscillating behavior below a fixed threshold value (y<=0.5). In our evaluation at most 10 discrete jumps are analyzed with a time horizon of 10 time units.
Steering Controller (nonlinear, hybrid): The simplified model of a steering controller was first proposed as a modular system [4]. The system models a steering controller, which aims at keeping a car close to the center of the lane. The lane is divided into seven regions, one for the center and symmetrically three regions left and right of the center depending on the distance to the lane center with different steering dynamics. As only the distance to the center of the lane is considered, the system dynamics in each of the seven locations can be described by two variables.
In the original version, a controller for the driving speed was considered as well; we omit this controller and assume constant speed or arbitrary speed from an interval and instead focus on the lane-keeping property of the system. In our work we consider three variations (ste_05, ste_10, and ste_RV) of the benchmark in which the speed of the vehicle is set to 5 m/s, 10 m/s, or may vary within the interval [5,10] m/s respectively. Though all instances contain potential Zeno behavior, trajectories for instance ste_05 should not leave the center region and thus Zeno behavior should not be present.
The specification used in the evaluation is similar to the original one in which the lane should never be left, i.e., the distance to the center of the lane should never exceed a certain boundary (here: 10 m). We use a time horizon of 30 time units and a maximum of 10 jumps.
Glycemic Control (nonlinear, hybrid): Coming from biology, this family of systems models the amount of blood-sugar over time under different models for insulin discharge [5,6,7]. Also this model is part of the ARCH benchmark collection [8]. Three different instances have been identified (gly_01, gly_02 and gly_03) which differ in their dynamics and number of locations (two, respectively three). This family of benchmarks was chosen, as it exhibits a larger state space dimension (four and five variables) than the other benchmarks for non-linear hybrid systems.
The goal in this benchmark is to show that the difference of the blood-sugar concentration to the base-value never exceeds a certain threshold. In the analysis we use a time horizon of 720 time units and a maximal jump depth of 10.
Spring-Pendulum (nonlinear, continuous): The model of a mass attached to a spring-pendulum is well-known in mechanics [9]. Being a continuous, non-linear system (pnd_01), this model uses transcendental functions to describe the dynamics of the system. In its original version, the dynamics are described as second-order differential equations over two variables—in the used version, the dynamics are converted to a system of first-order differential equations over four variables by adding the intermediate variables.
In our evaluation we used a time horizon of 10 time units. As there is no specification given our aim was to compute reachability only.
Table 1 below lists a few characteristic information for the considered benchmark instances. Further below, Table 2 provides the model specifications for all benchmark instances.
| Name | ODEs | Hybrid or continuous | Number of variables | Number of locations | Number of jumps |
| bld_48 | linear | continuous | 48 | 1 | 0 |
| plt_30 | linear | hybrid | 9 | 2 | 2 |
| plt_42 | linear | hybrid | 9 | 2 | 2 |
| flt_04 | linear | hybrid | 6 | 4 | 4 |
| flt_08 | linear | hybrid | 10 | 4 | 4 |
| flt_16 | linear | hybrid | 18 | 4 | 4 |
| flt_32 | linear | hybrid | 34 | 4 | 4 |
| ste_05 | non-lin | continuous | 3 | 7 | 12 |
| ste_10 | non-lin | hybrid | 3 | 7 | 12 |
| ste_RV | non-lin | hybrid | 3 | 7 | 12 |
| gly_01 | non-lin | hybrid | 5 | 3 | 4 |
| gly_02 | non-lin | hybrid | 5 | 3 | 4 |
| gly_03 | non-lin | hybrid | 4 | 2 | 1 |
| pnd_01 | non-lin | hybrid | 4 | 1 | 0 |
| Cora | Flow* | SpaceEx | DReach | Acumen | Hylaa | |
|---|---|---|---|---|---|---|
| bld_48 | model | model | model | model | model | model |
| plt_30 | model | model | model | model | model | model |
| plt_42 | model | model | model | model | model | model |
| flt_4 | model | model | model | model | model | model |
| flt_8 | model | model | model | model | model | model |
| flt_16 | model | model | model | model | model | model |
| flt_32 | model | model | model | model | model | model |
| ste_05 | model | model | not applicable | model | model | not applicable |
| ste_10 | model | model | not applicable | model | model | not applicable |
| ste_RV | model | model | not applicable | model | model | not applicable |
| gly_01 | model | model | not applicable | model | model | not applicable |
| gly_02 | model | model | not applicable | model | model | not applicable |
| gly_03 | model | model | not applicable | model | model | not applicable |
| pnd_01 | model | model | not applicable | model | model | not applicable |
10/fcx23n [4] Damm, W., Möhlmann, E., Rakow, A.: Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling. In: Proc. of HSCC’14, p. 145–150. ACM (2014). DOI 10/gg4tn5 [5] Bergman, R.N., Finegood, D.T., Ader, M.: Assessment of Insulin Sensitivity in Vivo. Endocrine Reviews 6(1), 45–86 (1985). DOI 10/brwjtx [6] Bergman, R.N., Ider, Y.Z., Bowden, C.R., Cobelli, C.: Quantitative Estimation of Insulin Sensitivity. American Journal of Physiology-Endocrinology and Metabolism 236(6), E667 (1979). DOI 10/gg4tnx
[7] Bergman, R.N., Phillips, L.S., Cobelli, C.: Physiologic Evaluation of Factors Controlling Glucose Tolerance in Man: Measurement of Insulin Sensitivity and Beta-cell Glucose Sensitivity from the Response to Intravenous Glucose. The Journal of Clinical Investigation 68(6), 1456–1467 (1981). DOI 10/dbfsqc [8] Chen, X., Schupp, S., Ben Makhlouf, I., Ábrahám, E., Frehse, G., Kowalewski, S.: A Benchmark Suite for Hybrid Systems Reachability Analysis. In: Proc. of NFM’15, pp. 408–414. Springer (2015). DOI 10/gg4tn3 [9] Meiss, J.D.: Differential Dynamical Systems, vol. 14. Siam (2007). DOI 10/dvgrwh