Tutorials
Below are tutorials for several of the available verification tools. They are intended to give a quick introduction to the software and are by no means comprehensive.
In each tutorial we attempt to verify a controller for stabilizing the trajectory of a car. This is a nice verification problem as it pertains to the rather intuitive example of a moving car, which can be modeled by a concise set of nonlinear differential equations. Being a nonlinear system, designing an appropriate controller is by no means trivial and we will see that there are trade-offs that one must consider before applying any of these tools.
SpaceEx
SpaceEx is a verification tool for linear hybrid systems. It implements two different reachability and safety analysis algorithms, the PHAver algorithm and the Le Guernic-Girard(LGG) algorithm. These can only analyze systems with piecewise affine dynamics, however, the LGG algorithm specifically uses operators with polynomial time complexity. This allows for the analysis of systems with over 100 variables (compared to 3-5 for most other algorithms). SpaceEx is also self-contained, freely downloadable as a virtual machine which can be run locally. It comes with a web-interface for setting up and executing its core algorithms, as well as a convenient GUI for specifying hybrid systems.
CORA
The COntinuous Reachability Analyzer, or CORA, is a MATLAB toolbox for the formal verification of linear-continuous, nonlinear-continuous, and hybrid systems. It uses various vector and matrix set representations to specify sets of initial conditions and parameters. These are then integrated with several reachability algorithms in order to construct an over-approximation of the potential evolution of the system state. The toolbox has a modular design, such that functions on the different set representation can easily be repurposed for other applications.
S-TALIRO
S-TALIRO is another Matlab toolbox which searches for trajectories of minimal robustness within either Simulink models or Matlab functions modeling a system. It uses stochastic optimization techniques such as Monte-Carlo methods to perform randomized testing with the aim of falsifying a system's safety specifications. Those specifications are entered using Metric Temporal Logic (MTL).
S-TALIRO is powerful in that it can handle continuous and discrete dynamical systems, hybrid automata, Matlab/Simulink functions, and hardware-in-the-loop models. It does not, however, perform formal verification. Instead it explores the space-robustness of a model through systematic testing.
Users may select from the following optimization algorithms: Simulated Annealing, Ant Colony Optimization, Genetic Algorithms and Cross Entropy. Additionally, it is straight forward to implement new stochastic optimization algorithms and incorporate them into the existing framework.