The Continuous Reachability Analyzer (CORA) is a collection of MATLAB classes
for the formal verification of cyber-physical systems using reachability analysis.
CORA 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 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.
From Release 2018 on, the direct import of SpaceEx models into CORA is also supported.
The following points summarize the main features of the CORA toolbox.
Reachability Analysis for Continuous Systems
CORA computes reachable sets for linear systems, nonlinear systems as well as
for systems with
constraints.
Continuous as well as discrete time models are supported. Uncertainty in the system inputs as
well as
uncertainty in the model parameters can be explicitly considered. In addition, CORA also
provides
capabilities for the simulation of dynamical models.
The toolbox is also capable to calculate the reachable sets for hybrid systems. All implemented dynamic
system classes can be used to describe the different continuous flows for the discrete system states.
Further, multiple different methods for the calculation of the intersections with guard sets are
implemented in CORA.
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 implements vector set representation,
e.g., intervals, zonotopes, Taylor models, and polytopes, as well as matrix set representations such as matrix
zonotopes and interval matrices.
CORA enables the formal verification of neural networks, both in open-loop as well as in closed loop scenarios. Open-loop verification
refers to the task where properties of the output set of a neural network are verified, e.g. correctly classified images given noisy
input. In closed-loop scenarios, the neural network is used as controller of a dynamic system and is neatly integrated in the
reachability algorithms above, e.g. controlling a car while keeping a safe distance.
Install the required packages described in Section 1.3 in the CORA manual
Run the following script in MATLAB:
Congratulations, you have successfully installed CORA!
Examples
CORA comes with plenty of examples to guide you through all components of CORA.
Explore them on GitHub,
or enjoy watching the playlist below showcasing the capabilities of CORA and check out the example script.