Guest Talk: Formal verification and learning of complex systems

Wednesday, May 23, 2018, 10:15am

Location: RWTH Aachen University, Department of Computer Science - Ahornstr. 55, building E3, room 9u10

 

Speaker: Alessandro Abate

 

Two known shortcomings of standard techniques in formal verification are the limited capability to provide system-level assertions, and the scalability to large-scale, complex models, such as those needed in Cyber-Physical Systems applications. This talk covers research which 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 the approach can be applied to complex physical systems for example, with spatially continuous variables, 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.