Couverture ElectroniqueS n°127

Issue d'un développement du CEA, la technologie Caveat mêle vérification par assertions et analyse du code pour réduire les coûts liés à la correction des bogues dans les logiciels critiques. L'explosion du premier lanceur Ariane 5 après moins d'une minute de vol, en 1996, ou la défaillance mortelle d'un missile antimissile Patriot lors de la première guerre du golfe montrent toute l'importance des conséquences des défaillances, et donc de la sûreté à mettre en &oelig;uvre, des logiciels critiques. Mais qu'entend-on par “ logiciel critique ” ? C'est un logiciel de petite taille, quelques dizaines de milliers de lignes de code à titre de comparaison, un logiciel comme Word contient entre 2 et 6 millions de lignes de code , et bien souvent écrit en C Ansi. Il se distingue par le fait qu'une erreur(*) dans son déroulement peut avoir un impact sur la sécurité des personnes ou de graves répercussions pour le système qu'il contrôle. « Le nombre de lignes de code relativement faible et le formalisme d'écriture simple (pour minimiser le risque d'erreurs) n'empêchent pourtant pas les logiciels critiques d'être de plus en plus complexes, ce qui rend leur vérification difficile, longue et coûteuse. L'étape de vérification peut représenter la moitié du coût de développement d'un système critique, voire jusqu'à 80 % dans l'aéronautique », constate Jacques Raguideau, chef du Laboratoire de sûreté des logiciels au Commissariat à l'énergie atomique (CEA).Une analyse valable quels que soient les paramètres d'exécutionLes méthodes de vérification actuelles, comme l'exécution du programme suivie de l'observation de son comportement ou les tests particuliers, ne sont plus vraiment adaptées. Les tests particuliers, la technique la plus couramment utilisée, consistent à réaliser plusieurs exécutions (analyse dynamique) avec des jeux donnés d'entrée estimés représentatifs des différents cas d'utilisation. Mais c'est là que le bât blesse. « Le nombre de tests qu'il faudrait effectuer pour être sûr et certain de la vérification du logiciel dépasserait les durées allouées à un projet. Les développeurs se limitent donc au test de cas estimés représentatifs de la réalité d'utilisation du système », regrette M. Raguideau.Avec Caveat, le CEA a développé une technologie de vérification valable quels que soient les paramètres d'exécution du logiciel critique il n'y a en fait pas d'exécution du logiciel (analyse statique du code) et basée sur la méthode de preuve des propriétés fonctionnelles. L'un des avantages est de pouvoir réaliser la vérification plus tôt dans le développement, réduisant ainsi considérablement le coût des corrections. Le coût de correction d'une erreur est en effet divisé par 10 entre le codage et les spécifications détaillées, et entre les spécifications détaillées et les spécifications. Le principe de fonctionnement de Caveat consiste à confronter le logiciel à vérifier à une propriété attendue du résultat, qui s'exprime par une formule mathématique de quelques lignes. « A partir de cette comparaison, Caveat énonce une condition mathématique. Il faut, par exemple, que le paramètre “ a ” soit inférieur à 0 pour que le résultat soit la valeur attendue. Le développeur vérifie que cette condition est vraie dans tous les cas d'utilisation. Si c'est le cas, la preuve est apportée que le résultat correspond à une propriété attendue. Si la preuve échoue, Caveat fournit les indications sur les raisons de l'échec. Il s'agit le plus souvent d'hypothèses insuffisantes qu'il faudra préciser. Cela conduit l'utilisateur à expliciter les non-dits », conclut M. Raguideau.(*) Il existe diverses sources d'erreurs liées à la perte de précision dans des calculs en virgule flottante, au blocage par attente réciproque, à la perte d'information par défaut de synchronisation, à des délais dépassés, à un résultat ne correspondant pas à ce qui est attendu ou à des erreurs d'exécution (bouclage infini, division par zéro, débord d'indice de tableau).Caveat : un développement du CEA commercialisé par TNI-ValiosysDix ans de recherche ont été nécessaires au Laboratoire d'intégration des systèmes et des technologies (List) du CEA pour mettre en &oelig;uvre le projet Caveat. Mais le CEA n'a pas été le seul à financer ce projet. Airbus et EDF ont également participé et utilisent déjà Caveat pour la vérification d'un logiciel des commandes de vol du programme A380 et pour un système de protection opérationnel sur certaines tranches nucléaires. En ce qui concerne la commercialisation en Europe et aux Etats-Unis, le CEA s'est tourné vers le Français TNI-Valiosys, avec qui il a signé, courant juillet, un accord de licence exclusive. « La technologie Caveat sera à la base de l'outil ImproveC pour la vérification de logiciels pilotant des applications industrielles embarquées critiques. Il viendra compléter notre catalogue d'outils de vérification matérielle et logicielle par preuve formelle tels qu'Improve-HDL, SDL et UML », précise Marc Frouin, p-dg de TNI-Valiosys.

Un logiciel met en garde les développeurs contre le risque d’erreurs dans les programmes critiques

Couverture ElectroniqueS n°127

IBM grave les premières puces en 2 nm en abandonnant les FinFET

Zeta, le protocole LPWAN made in China, arrive en Europe

Harting invente le connecteur électronique sur mesure

Un logiciel met en garde les développeurs contre le risque d’erreurs dans les programmes critiques

Dans la même rubrique

Couverture ElectroniqueS n°127

IBM grave les premières puces en 2 nm en abandonnant les FinFET

Zeta, le protocole LPWAN made in China, arrive en Europe

Harting invente le connecteur électronique sur mesure