End to end verification of Lyapunov stability at code level / Vérification bout en bout de la stabilité d'un contrôleur au niveau du code
Il s’agit d’utiliser différents outils pour prouver automatique la stabilité d’un contrôleur à temps discret au niveau du code. L’idée sous-jacente est de pouvoir compiler les preuves comme on compile les modèles ou le code. Ainsi le modèle initial en Simulink est enrichi par un argument de stabilité, une fonction de Lyapunov. La preuve de stabilité est ensuite compilée sous la forme d’une annotation de code Lustre, puis de code C. L’objectif de ce stage est d’automatiser le processus.
Objectif/Objective
The objective of this project is to prove the capability at Simulink level to perform a proof a stability and validate it both at model level and at code level. While, in this simple setting, the approach has been solve in theory, no tool is currently able to perform that proof automatically. The goal of this internship is to combine tools and develop missing parts of the approach to enable such an automatic proof.
L’objectif de ce projet est de s’intéresser à la mise en oeuvre automatique de la preuve de stabilité d’un système linéaire depuis Simulink jusqu’au code. Théoriquement ce problème est résolu et a été appliqué sur des cas simples, mais toujours manuellement. Aucun outil n’est capable aujourd’hui de traiter ce problème. Le but de ce stage est de combiner les outils existants et de développer les parties manquantes de l’algorithme afin de permette l’analyse automatique de tels systèmes.
Outils
CocoSim / LustreC
Depuis quelques années, en collaboration avec NASA Ames, nous développons CocoSim, une boîte à outils open-source pour Matlab Simulink. Cette boîte à outils est essentiellement motivée par les problématiques de vérification de modèles Simulink mais est entièrement construite sur une architecture de compilateur.
Ainsi, grâce à CocoSim, on peut compiler un modèle Simulink discret en code C et utiliser ensuite ce code C pour effectuer des simulations ou pour l’exécuter sur le système embarqué.
LustreC est un compilateur écrit en Caml qui compile les modèles Lustre générés par CocoSim en code C.
Frama-C
Frama-C est une plateforme de vérification de code C. C’est un outil open-source développé par le CEA.
Optimization convexe
On utilisera différent outils qui facilitent l’utilisation de l’optimisation convexe.
- Yalmip en Matlab
- OSDP en Caml
Qui utilisent les solveurs suivants: Mosek, CSDP, SDPT3
Travail à fournir / Tasks
Il faut pouvoir réaliser d’abord de façon manuelle, puis, ensuite, de façon automatique le processus suivant:
- pour un modèle Simulink simple (par exemple un système linéaire) construire un invariant, une fonction de Lyapunov
- Enrichir le modèle pour intégrer la spécification
- Préserver cette information lors de la compilation jusqu’au code C
- Valider, au niveau du code, l’invariant exprimé sur l’implémentation de la loi du modèle.
Dans la première phase, il s’agira d’utiliser les outils disponibles. Pour automatiser l’approche il faudra étendre les outils CocoSim et LustreC pour prendre en compte ce type d’invariants.
Pre-requis / Requirements
- Programmation en Ocaml
- Connaissance en optimisation
- Connaissance de Matlab/Simulink
