< Retour au sommaire

Formal Verification of Control System Software

Pierre-Loïc Garoche le

Lieu: https://app.livestorm.co/cea_list/seminaire-pierre-loic-garoche?type=light

In this talk we will present an approach to apply formal verification techniques, from the theoretical computer science community, to the specific class of control system software and closed-loop control models. All analyses are performed in the state-space domain, easing the code level interpretation of the result. Among the different formal verification techniques, abstract interpretation, introduced by Cousot and Cousot in the 70s, is a static analysis technique that formulates verification goals as set membership. We proposed to rely on different mathematical tools such as convex optimization or affine arithmetics to compute such sets and therefore to guarantee formally and exhaustively properties over the control systems and control software.