Room 248, IMAG
19 décembre 2018 - 14h00
Simulating and Verifying Cyber-Physical Systems: Current Challenges and Novel Research Directions
par Khalil Ghorbal de INRIA
19 décembre 2018 - 14h00
Simulating and Verifying Cyber-Physical Systems: Current Challenges and Novel Research Directions
par Khalil Ghorbal de INRIA
Abstract: Modeling real-life applications require the ability to combine continuous and discrete behaviors at once. The behavior of physical components, governed by electrical and kinetic laws, are naturally represented as continuous solutions of differential equations. It contrasts with several inherently discrete phenomenon such as controllers’ commands, modes switching, or mechanical impacts. For instance, modeling a mid-air collision avoidance system that advises the pilot to go upward or down- ward to avoid a detected nearby airplane requires mixing the continuous motion of the aircraft with the discrete decisions suggested by the system to resolve the conflict. The need to model, simulate and automatically analyze such systems in a compositional fashion has never been as important as nowadays, and it is perhaps one of the major challenges of the twenty first century. After a brief overview of the current state-of-the-art in modeling paradigms, simulation and verification of hybrid systems, the presentation will highlight two specific challenges we believe of great importance. The first is the automated generation and verification of invariant properties, that are those quantities that do not vary with respect to time. To some extent, this first challenge can be thought of as a generalization of the perhaps much familiar notion of fixed-points in the standard settings of imperative programs. The second challenge concerns the operational semantics of component-based modeling languages. Those languages are well suited to model multi-physics systems as they combine algebraic constraints, resulting from the laws of physics, in interaction with the non-smooth behavior like impact laws. Yet, the correct simulation of such hybrid models poses several subtle problems that require a careful attention. Several concrete examples will be used throughout the talk to highlight the difficulties and appreciate the several research directions we are currently exploring.
