https://veri-bbb.imag.fr/b/rad-ofn-9t8-rqc
3 décembre 2021 - 10h00
Design, Verification and Synthesis of Hybrid Systems.
par Miriam Garcia de Institute of Science and Technology (IST) of Austr
Abstract: We have witnessed an increasing interest and investment in safe autonomous systems such as self-driving vehicles, robots and medical devices. Critical aspects to be considered in the design of these complex systems are security, reliability and safety. For instance, a single design bug can wreak havoc across thousand of deployed devices. The prevention of such occurrences requires the use of a rigorous methodology to validate and verify pivotal properties in autonomous systems.
Current approaches to verify and validate software and systems rely mainly on testing and simulation. These solutions encounter in general two problems, they are not cost-efficient and do not provide a correctness certificate for the system performance. To design high-confidence systems, solid modelling formalisms along with verification and validate algorithms have been developed in the field of computer science. These techniques fall into the discipline known as formal methods, which has its foundations in rigorous mathematical modelling and analysis.
The broad goal of my research is to design and analyse real-world autonomous systems, by developing cost-efficient formal approaches which provide correctness certificates. Concretely, this talk will introduce some of the algorithmic techniques I have developed so far, such as (1) a Counterexample Guided Abstraction Refinement (CEGAR) approach for stability verification of hybrid systems, (2) a stabilizing controller synthesis of hybrid systems, and (3) techniques for the data-based synthesis of hybrid automata.
