I discuss a new and formal, measurement-driven and model-based automated verification and synthesis technique, to be applied on quantitative properties over systems with partly unknown dynamics. I focus on physical systems (with spatially continuous variables, possibly noisy), driven by external inputs and accessed under noisy measurements, and suggest that the approach can be as well generalised over CPS. I formulate this new setup as a data-driven Bayesian model inference problem, formally embedded within a quantitative, model-based verification procedure. While emphasising the generality of the approach over a number of diverse model classes, this talk zooms in on systems represented via stochastic hybrid models (SHS), which are probabilistic models with heterogeneous dynamics (continuous/discrete, i.e. hybrid, as well as nonlinear) - as such, SHS are quite a natural framework for CPS. With focus on model-based verification procedures, I provide the characterisation of general temporal specifications based on Bellman’s dynamic programming. The computation of such properties and the synthesis of related control architectures optimising properties of interest, is attained via the development of abstraction techniques based on quantitative approximations. Theory is complemented by algorithms, all packaged in a software tool (FAUST^2) that is freely available to users.
Alessandro Abate is an Associate Professor in the Department of Computer Science at the University of Oxford. He received a Laurea degree in Electrical Engineering (summa cum laude) in October 2002 from the University of Padova. As an undergraduate He also studied at UC Berkeley and RWTH Aachen. He earned an MS in May 2004 and a PhD in December 2007, both in Electrical Engineering and Computer Sciences, at UC Berkeley, working on Systems and Control Theory with S. Sastry. Meanwhile he was an International Fellow in the CS Lab at SRI International in Menlo Park (CA). Thereafter, he has been a PostDoctoral Researcher at Stanford University, in the Department of Aeronautics and Astronautics, working with C. Tomlin on Systems Biology in affiliation with the Stanford School of Medicine. From June 2009 to mid 2013 he has been an Assistant Professor at the Delft Center for Systems and Control, TU Delft - Delft University of Technology, working with my research group on Verification and Synthesis over complex systems and on Systems Biology.
This talk is organized by the Cyber-Physical Systems Group at the Institute of Computer Engineering.