DS07 - Société de l'information et de la communication

Preuves formelles pour systèmes temps-réel – RT-proofs

Résumé de soumission

Les systèmes temps-réel se trouvent au cœur de la plupart des
technologies critiques modernes, y compris l'avionique, l'automobile
et la robotique. Pour s'assurer qu'ils réagissent dans le temps voulu
même au pire cas, des efforts de validation rigoureux sont
nécessaires, basés sur des techniques d'analyse temporelle
sophistiquées.

Toutefois, les méthodes d'analyse actuelles manquent de rigueur, elles
s'appuient seulement sur des preuves informelles qui sont difficiles à
suivre, vérifier ou réutiliser, d'où un risque d'erreurs subtiles mais
fatales. C'est ainsi qu'un nombre alarmant de résultats erronés a dû
être corrigé ces dernières années. Parmi les plus remarquables,
l'analyse temporelle du bus CAN (utilisé dans la plupart des voitures
modernes) a été réfutée 13 ans après sa publication initiale.

En utilisant l'assistant de preuve Coq, le projet RT-proofs posera les
fondations de la vérification assistée par ordinateur de résultats
d'analyse temporelles. RT-proofs augmentera fondamentalement le niveau
de rigueur, au bénéfice tant de la communauté académique que des
développeurs d'outils.

Coordinateur du projet

ONERA (Divers public)

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

VERIMAG
Max Planck Institute for Software Systems
TU Braunschweig
ONERA
Centre de Recherche Inria Grenoble - Rhône-Alpes

Aide de l'ANR 742 112 euros
Début et durée du projet scientifique : octobre 2017 - 36 Mois

Liens utiles