Alessandro Abate

KEYNOTE 

Learning and Verification of complex systems: model-based and data-driven methods

Abstract: Two known shortcomings of standard techniques in formal verification are their limited capability to provide system-level assertions, and their practical scalability to large, complex models, such as those needed in modern applications concerning Cyber-Physical Systems or Digital Twins. This talk covers a research line that addresses these shortcomings by bringing model-based and data-driven methods together, which can help pushing the envelope of existing algorithms and tools in formal verification. 

In the first part of the talk, I will discuss a new, formal, measurement-driven and model-based automated technique, for the quantitative verification of systems with partly unknown dynamics. I will formulate this setup as a data-driven Bayesian inference problem, formally embedded within a quantitative, model-based verification procedure. I argue that this new approach can be applied to complex systems, driven by external inputs and accessed under noisy measurements. In the later part of the talk, I will concentrate on using actions in a model to perform active learning, namely to extract max information from the underlying system towards the quantitative verification of a given property. I shall conclude arguing that this mix of model-based and data-driven methods can be useful in the context of formal reasoning over applications concerning Digital Twins.