Actualité web & High tech sur Usine Digitale

Recevez chaque jour toute l'actualité du numérique

x

Adacore et l'Inria créent un laboratoire pour démocratiser les méthodes de test formel

ProofInUse est un nouveau laboratoire créé par Adacore, éditeur de logiciels libres spécialiste du langage Ada, et l’Inria (Institut national de recherche en informatique et automatique). Son objectif : démocratiser les méthodes de test par preuves formelles dans le développement de logiciels critiques.
Twitter Facebook Linkedin Flipboard Email
×

Adacore et l'Inria créent un laboratoire pour démocratiser les méthodes de test formel
Adacore et l'Inria créent un laboratoire pour démocratiser les méthodes de test formel © AdaCore

Les preuves formelles sont l’un des grands défis de ces prochaines années dans l’aéronautique, le spatial et la défense. Elles sont autorisées depuis peu par les organismes de certification, mais trop rares sont les industriels qui les utilisent. Aujourd’hui, les logiciels critiques (commandes de vol, par exemple) sont soumis à d’énormes batteries de tests pour s’assurer qu’ils ne contiennent aucun bug. Ces tests sont longs et non exhaustifs.

La méthode par preuve formelle, quant à elle, revient à considérer chaque ligne de code comme une équation, et à prouver par des théorèmes mathématiques qu’un "plantage" du logiciel est impossible. "C’est un bon moyen de réduire les temps de tests et les coûts de vérification tout en améliorant la sûreté des logiciels", résume Cyrille Comar, président d’Adacore, éditeur français spécialiste des outils de développement en langage Ada (un langage très utilisé dans le monde des logiciels critiques).

Un baromètre de la qualité du code

Adacore travaille depuis 2010 avec des chercheurs de l’Inria (Institut national de recherche en informatique et automatique). Le fruit de cette collaboration est Spark 2014, un environnement de développement pour logiciels critiques en Ada qui intègre des fonctions de preuves formelles. L’équivalent de l’outil Frama C pour le langage C. "En phase de tests, il indique si le programme est bien écrit et met en évidence les erreurs", indique Claude Marché, professeur à l’Inria et directeur du laboratoire ProofInUse.

Le nouveau laboratoire commun à Adacore et l’Inria a obtenu un financement de l'agence nationale de la recherche jusqu’en 2017. Il comptera à terme trois chercheurs et cinq ingénieurs, avec un objectif double : poursuivre la recherche académique, et convaincre les industriels de l’intérêt des méthodes formelles. Côté recherche, il s’agira surtout d’améliorer les fonctions automatiques du logiciel, notamment la fonction qui surligne chaque ligne de code en rouge, orange ou vert selon la qualité du programme. Côté industriel, "il faudra élargir l’adoption des méthodes formelles à d’autres secteurs, comme les transports terrestres, et rendre ces méthodes accessibles à des utilisateurs non mathématiciens", lance Claude Marché.

Une annonce qui ne manque pas de susciter la curiosité de certains industriels français. Airbus Defence & Space, ainsi que Thales, ont affirmé leur intention d’étudier de près les réductions de coûts sur les tests logiciels rendues possibles par les méthodes formelles.

Frédéric Parisot

Réagir

* Les commentaires postés sur L’Usine Digitale font l’objet d’une modération par l’équipe éditoriale.

 
media
Suivez-nous Suivre l'Usine Digitale sur twitter Suivre l'Usine Digitale sur facebook Suivre l'Usine Digitale sur Linked In RSS Usine Digitale