- University of Verona
mercoledì 30 maggio 2018
In many applicative fields there is the need to model and design 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 because of their mixed
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. We describe an open-source framework
for hybrid system verification, called ARIADNE, developed by a joint team
led by the University of Verona, which exploits approximation techniques
based on the theory of computable analysis for implementing formal
verification algorithms. ARIADNE can be used to verify complex hybrid
systems, supporting an assume-guarantee reasoning approach.
The library has been tested in some interesting critical applications
(e.g., for verification of plans in robotic surgery) and it is in full
development, posing challenging research problems that call for active
involvement by students and researchers interested in scientific computing
and modeling of dynamical systems.