Formal verification of nonlinear hybrid systems: the release of Ariadne 1.0


Tiziano Villa and Luca Geretti

Presentation title

Formal verification of nonlinear hybrid systems: the release of Ariadne 1.0

Authors

Tiziano Villa and Luca Geretti

Institution(s)

University of Verona

Presentation type

Technical presentation

Abstract

In embedded systems design there is often the need to model complex systems having a mixed discrete and continuous behaviour that cannot be characterized faithfully using either discrete or continuous models only. Such systems consist of a discrete control part that operates in a continuous environment and are named hybrid systems. Unfortunately, most of the verification problems for hybrid systems, like reachability analysis, turn out to be undecidable. Because of this, many approximation techniques and tools to estimate the reachable set have been proposed in the literature. However, most of the tools are unable to handle nonlinear dynamics and constraints and have restrictive licenses. In this paper we present the first official release of an open-source framework for hybrid system verification, called ARIADNE, which exploits approximation techniques based on the theory of computable analysis for implementing formal verification algorithms.


Additional material

  • Presentation slides: [pdf]

  • Warning: Undefined variable $ADDITIONAL_MATERIAL in /var/www/html/iwes/2017/presentations.phtml on line 79