​Le point commun entre des logiciels de commandes de vol, de surveillance de réacteur nucléaire, ou encore de signalisation ferroviaire ? Tous sont des logiciels dits « critiques », qui doivent être non seulement exempts de bugs, mais aussi résistants aux cyber attaques.

Les outils de vérification des logiciels critiques formulent en général trois types de réponses : « oui, le logiciel testé est sûr », « non, il ne l'est pas » ou « peut-être ne l'est-il pas ». Dans ce dernier cas, les outils existants fournissent énormément d'informations, très difficiles à restituer de manière compréhensible et synthétique et donc à interpréter pour y trouver l'origine des bugs éventuels. Ce qui revient à chercher une aiguille dans une botte de foin !

Avec Ivette, basée sur leur plateforme d'analyse de code Frama-C, les chercheurs du CEA-List ont conçu un environnement logiciel inédit et évolutif pour enrichir l'expérience utilisateur des ingénieurs de vérification logicielle. S'inspirant de méthodes de visualisation et de fouille de données issues des technologies du web 3.0, Ivette leur permet d'explorer les résultats d'analyse de manière pertinente et interactive. Mais également de mieux piloter l'analyse pour optimiser les chances d'arriver à une réponse positive ou négative.

Atout-clé : Ivette, environnement open source, peut intégrer divers outils d'analyse de code pour les faire collaborer avec Frama-C…ou faciliter l'intégration de Frama-C aux environnements industriels ! La première version a déjà été livrée à deux partenaires majeurs du CEA-List et un nouvel usage est déjà envisagé, en utilisant Ivette comme support à la formation des ingénieurs et experts du domaine.