Formal Verification of Nonlinear Hybrid Systems using Ariadne

ABSTRACT: In embedded systems design there is often the need to model complex systems having a mixed discrete and continuous behavior 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 do not perform conservative numerical rounding. In this seminary we present 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.

BIO: Davide Bresolin received the Ph.D. degree in computer science from the University of Udine, Udine, Italy, in 2007. He is an Assistant Professor with the Mathematics Department, University of Padova, Italy. From 2007 to 2013, he was a Research Fellow with the Department of Computer Science, University of Verona, Verona, Italy, where he collaborated with the Electronic Systems Design Group (ESD) and the ALTAIR Robotics Group. From 2013 to 2016 he was an Assistant Professor with the Computer Science and Engineering Department, University of Bologna, Bologna, Italy. His research activity is focused on formal verification of cyber-physical and embedded systems using hybrid automata and temporal logics, on automata theory, and on temporal representation and reasoning using interval-based temporal logics.

Luca Geretti received the Laurea degree in electrical engineering and the Ph.D. degree in computer engineering from the University of Udine, Udine, Italy, in 2005 and 2009, respectively. He was a Research Fellow with the Department of Computer Science, University of Verona, Verona, Italy, between 2009 and 2011. He was a Research Fellow with the Department of Electrical Engineering, University of Udine, Udine, Italy, between 2012 and 2015. He is currently a Research Fellow with the Department of Computer Science, University of Verona, Verona, Italy. His current research interests are in the fields of formal verification of cyber-physical systems using hybrid automata, and of parallel and distributed computing.

Hosted by: Pierluigi Nuzzo