Preuves formelles pour systèmes temps-réel – RT-proofs
Preuves formelles pour systèmes temps-réel
Les systèmes temps-réel se trouvent au coeur des systèmes critiques<br />modernes. Pour garantir leur comportement temporel, des efforts de<br />validation rigoureux sont nécessaires.<br /><br />Toutefois, les méthodes d'analyse actuelles manquent de rigeur et un<br />nombre alarmant de résultats incorrects a dû être corrigé au cours des<br />dernières années. En utilisant l'assistant de preuve Coq, le projet<br />RT-proofs pose les fondations de la vérification assistée par<br />ordinateur des résultats d'analyses temporelles.
Contexte et motivation
Les systèmes temps-réel sont des systèmes qui doivent satisfaire<br />des exigences temporelles telles des bornes de temps de réponse,<br />c'est à dire des bornes sur le temps maximum nécessaire à une<br />tâche logicielle pour terminer son exécution une fois qu'elle a<br />été activée. C'est systèmes sont omniprésents dans nos vies, des<br />voitures aux avions en passant par les téléphones<br />portables. Établir des propriétés temps-réel, telles des bornes<br />sur le temps maximum nécessaire à un système pour répondre à un<br />stimulus donné, est un challenge non trivial car les tâches<br />s'exécutant sur le même processeurs ou sur des processeurs<br />différents peuvent avoir une influence temporelle complexe les<br />unes sur les autres du fait par exemple de l'ordonnancement, de<br />ressources partagées, de contraintes de précédence ou<br />d'interférences liées aux communications.<br /><br />Il existe de nos jours un grand ensemble de travaux de recherche<br />sur les méthodes d'analyse de systèmes temps-réel. Toutefois, les<br />preuves sous tendant toutes ces analyses sont trop souvent plus<br />ou moins informelles ou difficiles à vérifier. Comme<br />illustration, malgré un usage très répandu, l'analyse SPNP<br />originale comportait une erreur fondamentale qui ne fut<br />découverte que plusieurs années après sa publication<br />initiale. D'autres exemples d'analyse de pire cas incorrectes<br />allant de l'erreur d'une unité aux généralisations incorrectes en<br />passant par des énoncés purement faux abondent dans la<br />littérature. Pire, même lorsque la théorie sous jacente est<br />correcte, il n'existe toujours aucune garantie qu'elle est<br />implémentée correctement dans les chaînes d'outils utilisée en<br />pratique. En résumé, l'état de l'art de l'analyse de systèmes<br />temps-réel critique laisse beaucoup à désirer. L'usage de preuves<br />papier informelles est tout simplement inadapté.
Pour garantir la viabilité et la pertinence en pratique des
analyses de systèmes temps-réel pour la certification des
systèmes critiques, une base formelle solide et digne de
confiance est nécessaire. L'usage d'un assistant de preuve tel
que Coq pour formaliser ces fondations permet d'atteindre le
niveau de confiance requis tout en simplifiant la revue par les
pairs de résultats futurs de complexité croissante puisque seules
les spécifications nécessitent une revue tandis qu'on peut faire
confiance aux preuves. La décénnie passée a montré que les
assistants de preuve ont atteint un niveau d ematurité qui les
rend utilisables pour les grand systèmes considérés. De plus, des
résultats initiaux dans le domaine temps-réel ont déjà été
obtenu.
En outre, les outils commerciaux implémentant les analyses
temps-réel de l'état de l'art, comme SymTA/S, NETCAR-Analyzer ou
RTaW Pegase ne peuvent garantir formellement la correction des
résultats qu'ils produisent. Ceci est en partie dû au manque de
support formel des analyses elles même mais résulte également de
l'effort qui serait nécessaire pour certifier des outils si
complexes. Étant donné que les exigences de certification et de
sureté évoluent constamment (en particulier dans le secteur
automobile, un secteur clef pour les producteurs d'outils
temps-réel, avec l'arrivée de la norme ISO26262), ce fossé de
certification s'annonce comme un obstacle majeur avec des
implications conséquentes dans l'industrie de l'embarqué. Pour
s'attaquer à ce problème, le projet RT-proofs vise à certifier
les résultats des analyses, plutôt que de certifier les outils,
en posant les fondations pour la génération, la composition et la
vérification de certificats de preuve pour des bornes de temps de
réponse et de délais de bout en bout.
L'essentiel du travail réalisé dans le projet RT-proofs vise à être
formellement spécifié et prouvé en utilisant l'assistant de preuve Coq
dans la librairie Prosa, librement disponible à l'adresse
prosa.mpi-sws.org
Parmi les résultats actuels du projet, on peut noter
- Une compréhension des concepts communs nécessaires pour décrire
formellement le comportement des systèmes temps-réel et les concepts
de modélisation habituels ;
- Des résultats initiaux connectant les modèles utilisés et les
résultats produits par les analyses CPA (Compositional Performance
Analysis) et NC (Network Calculus) ;
- Une formalisation du principe de «busy-window« et l'analyse de temps
de réponse correspondante
- CertiCAN, un outil réalisé avec Coq pour la certification formelle
de résultats d'analyse CAN.
Les travaux réalisés dans le projet sont présentés dans de multiples
publications. La liste complète et maintenue à jour se trouve sur le
site web du projet (https://rt-proofs.inria.fr/publications/).
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.
Coordination du projet
Pierre Roux (ONERA)
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 VERIMAG
MPI-SWS Max Planck Institute for Software Systems
TUBS TU Braunschweig
ONERA
INRIA GRA Centre de Recherche Inria Grenoble - Rhône-Alpes
Aide de l'ANR 742 111 euros
Début et durée du projet scientifique :
octobre 2017
- 36 Mois
