You are here: Home › Tools › Hybrid systems › Guided Model Checking for Hybrid …

Guided Search for Hybrid Systems Based on Coarse-Grained Space Abstractions

Contents

  1. Overview
  2. Navigation Benchmark
  3. Satellite Benchmark
  4. Download
  5. References

Overview

Hybrid systems represent an important and powerful formalism for modeling real-world applications that require both discrete and continuous behavior. A verification tool such as SpaceEx is based on the exploration of a symbolic search space (the region space). As a verification tool, it is typically optimized towards proving the absence of errors. In some settings, e.g., when the verification tool is employed in a feedback-directed design cycle, one would like to have the option to call a version that is optimized towards finding an error path in the region space. A recent approach in this direction is based on guided search. Guided search relies on a cost function that indicates which states are promising to be explored, and preferably explores more promising states first. In this paper, we introduce an abstraction-based cost function based on pattern databases for guiding the reachability analysis. For this purpose, we introduce a suitable abstraction technique that exploits the flexible granularity of modern reachability analysis algorithms. Our cost function is an effective extension of pattern database approaches that have been successfully applied in other areas. We have implemented our approach in the SpaceEx model checker. Our evaluation shows its practical potential. The journal paper extends the conference paper [2] which appeared in SPIN2013. 

Navigation Benchmark

We consider a variant of the well-known navigation benchmark [3]. This benchmark models an object moving on the plane which is divided into a grid of cells. The dynamics of the object's planar position in each cell is governed by the differential equations $\dot{x}=v$, $\dot{v}=A(v-v_d)$ where $v_d$ stands for the targeted velocity in this location. Compared to the originally proposed navigation benchmark problem, we address a slightly more complex version with the following additional constraints. First, we add inputs allowing perturbation of object coordinates, i.e., the system of differential equations is extended to: $\dot{x}=v+u$, $\dot{v}=A(v-v_d)$ , $u_{min} \le u \le u_{max}$ . Second, to make the search task even harder, the benchmark problems also feature obstacles between certain grid elements. This is particularly challenging because, in contrast to the original benchmark system, one can get stuck in a cell where no further transitions can be taken, and consequently, backtracking might become necessary. The size of the problem instances varies from 400 to 900 locations, and all instances feature 4 variables.

Satellite Benchmark

This benchmark class is a good example of hybridization technique. For a hybrid system with nonlinear continuous dynamics, hybridization is a technique for generating a hybridized system from the original one. The hybridized automaton has simpler continuous dynamics (usually affine or rectangular) that over-approximate the behavior of the original automaton, and can be analyzed by SpaceEx. For our evaluation, we consider benchmarks from this hybridization technique applied to nonlinear satellite orbital dynamics, where two satellites orbit the earth with nonlinear dynamics described by Kepler's laws. For more details, we refer to the work of Johnson et al. [4]. The size of the problem instances varies from 36 to 1296 locations, and all instances feature 4 variables. The verification problem is conjunction avoidance, i.e., to determine whether there exists a trajectory where the satellites come too close to one another and may collide.

Tank Benchmark

This benchmark consists of variants of the tank benchmark [5,6]. The tank benchmark consists of some $N\in\mathbb{N}$ tankes, where each tank $i \in \{1,\ldots,N\}$ loses volume $x_i$ at some constant flow rate $v_i$, so tank $i$ has dynamics $\dot{x}_i = -v_i$, for a real constant $v_i \geq 0$. One of the tanks is filled from an external inlet at some constant flow rate $w$, so it has dynamics $\dot{x}_i = w - v_i$, for a real constant $w \geq 0$. In our variant, the volume lost by each tank simply vanishes and does not move from one tank to another. This benchmark class is qualitatively different than either the navigation or sateillite benchmarks, as the discrete state space may be small. However, there is nondeterminism in which tank to fill at a given instance.

Heater Benchmark

This benchmark consists of variants of the heater benchmark [3]. In our variation, we consider three rooms with three heaters. Each room is modeled as an automaton with two locations, where the heater is either on or off. The composite heater system is the composition of these three room automata. The size of the problem instances have 8 locations, and all instances feature 3 temperature variables, 1 time variable, and 16 real constants.

Download

Click here to download the archive which has the following structure :

  1. spaceex-64bit - 64-bit SpaceEx binary and libries
  2. navigation-benchmark - Instances of the navigation benchmark and scripts
  3. satellite-benchmark - Instances of the satellite benchmark and scripts
  4. tank-benchmark - Instances of the tank benchmark and scripts
  5. heater-benchmark - Instances of the heater benchmark and scripts
Furthermore, in both folders navigation-benchmark and satellite-benchmark you can find a README file describing in details steps to run the analysis of benchmarks and plot the results. If you would like to get the source code of SpaceEx or have any questions, please contact Sergiy Bogomolov.

References

  1. Guided Search for Hybrid Systems Based on Coarse-Grained Space Abstractions, Sergiy Bogomolov, Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor T. Johnson, Hamed Ladan, Andreas Podelski and Martin Wehrle, submitted to STTT 2014
  2. Abstraction-Based Guided Search for Hybrid Systems, Sergiy Bogomolov, Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor T. Johnson, Hamed Ladan, Andreas Podelski and Martin Wehrle, SPIN 2013
  3. Benchmarks for hybrid systems verification, Ansgar Fehnker and Franjo Ivančić, HSCC2004
  4. Satellite rendezvous and conjunction avoidance: Case studies in verification of nonlinear hybrid systems, Taylor T. Johnson, Jeremy Green, Sayan Mitra, Rachel Dudley, and R. Scott Erwin, FM 2012
  5. Modularity for timed and hybrid systems, Rajeev Alur, Thomas A. Henzinger, CONCUR 1997
  6. On the regularization of zeno hybrid automata, Karl Henrik Johanssona, Magnus Egerstedtb, John Lygerosa, Shankar Sastry, Systems & Control Letters 1999