Toolbox Description

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 capabilities 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.

  • Reachability Analysis for Hybrid Systems

    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.

  • Geometric Sets

    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., zonotopes, Taylor models and intervals, as well as matrix set representations such as matrix zonotope and interval matrices.

PLACEHOLDER

Publications

[1] M. Althoff, D. Grebenyuk and N. Kochdumper. Implementation of Taylor Models in CORA 2018. In Proc. of the 5th International Workshop on Applied Verification for Continuous and Hybrid Systems, pages 145–173, 2018. [ .bib | .pdf ]
[2] M. Althoff and D. Grebenyuk. Implementation of interval arithmetic in CORA 2016. In Proc. of the 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems, pages 91-105, 2016. [ .bib | .pdf ]
[3] M. Althoff. An introduction to CORA 2015. In Proc. of the Workshop on Applied Verification for Continuous and Hybrid Systems, pages 120-151, 2015. [ .bib | .pdf ]
[4] M. Althoff. Guaranteed State Estimation in CORA 2021. In Proc. of the Workshop on Applied Verification for Continuous and Hybrid Systems, pages 161-175, 2021. [ .bib | .pdf ]