Frequently Asked Questions
This document provides some answers to common questions about SpaceEx.
General Questions
What is SpaceEx and what makes it special?
SpaceEx is a verification tool for hybrid systems. The goal is to verify (ensure beyond reasonable doubt) that a given mathematical model of a hybrid system satisfies the desired safety properties. The basic functionality is to compute the sets of reacheable states of the system. A general introduction to the topic is available from Oded Maler.
Strictly speaking, SpaceEx is a development platform on which several different verification algorithms are implemented. Our current favorite is our implementation of the LeGuernic-Girard (LGG) algorithm (Colas Le Guernic and Antoine Girard. Reachability analysis of linear systems using support functions. Nonlinear Analysis: Hybrid Systems, 4(2):250-262, 2010.). Classic reachability algorithms use operators whose computational cost is exponential in the number of continuous variables, which limits them to systems with 3-5 continuous variables for nontrivial dynamics. The operators of the LeGuernic-Girard algorithm are polynomial, and systems with 100 variables and more have been analyzed that way.
Who's behind SpaceEx?
SpaceEx is being developed by the Hybrid Systems group of Oded Maler at Verimag labs in Grenoble, France. The development team is led by Goran Frehse.
What kind of dynamics can SpaceEx handle, and what other restrictions are there on models?
The LGG algorithm works for dynamics of the form dx/dt = Ax + Bu, where u is a set of nondeterministic input variables that may be constrained by inequalities. Similarly, transitions may reset variables with equations of the form x := Ax + Bu.
Invariants and guards must be conjunctions of linear inequalities or equations. All transitions must have labels.
How can I run SpaceEx?
There are two ways to run SpaceEx, see the download section:
- You can download the virtual machine server, and run SpaceEx from a web-browser that connects to the server.
- You can download the executable and run it under certain versions of Linux using the command line.
Note that we don't provide executables for Windows, Mac, or other operating systems. If the provided executable doesn't work for you, please use the virtual machine server.
Are SpaceEx results formally sound? Are they useless if they're not?
That depends on the scenario. The PHAVer scenario is formally sound. It uses unbounded integer arithmetic and guaranteed overapproximations, so if the analysis terminates, the output is an overapproximation of the reachable states.
The LGG scenario is not numerically sound, since double precision floating point computations are used to represent sets of states and solve the differential equations. This choice was made to achieve scalability. While the results are, on a strictly formal level, unsound, we consider them nonetheless useful for finding bugs in a system's design: If undesired behaviour is found using the LGG scenario, the user will likely validate or invalidate this "bug" on a more detailed model or on the implementation. Should the bug turn out to be spurious, numerical inaccuracies will be only one aspect in a whole series of simplifications and overapproximations that made the model verifiable in the first place. If on the other hand the LGG scenario finds the system safe, we can only conclude that more sophisticated methods are necessary to find bugs for that system.
How to visualize SpaceEx output?
- The SpaceEx server can generate GIF and pdf images of two-dimensional graphs.
- For 2D output, SpaceEx generates .gen files, which are lists of vertices of polyhedra, the polyhedra being separated by a blank line. The file can be processed by graph, or read in MATLAB using this little script.
- For 3D output, SpaceEx generates .jvx files. They can be displayed using JavaView or JReality Viewer. JReality produces a high quality image of the scene using the integrated Sunflow renderer (menu File/Export/Sunflow...).
