La société franço-américaine AdaCore, fournisseur d'outils et de services de développement logiciel à haute intégrité, lance avec GNAT Foundry: Intersection un démonstrateur en open source illustrant la collaboration entre ingénieurs humains et outils d’intelligence artificielle (IA) pour la création de logiciels de haute intégrité.

Cette démonstration montre comment les méthodes formelles et des outils déjà éprouvés sur le terrain peuvent guider l'IA au sein d'un flux de travail de développement logiciel.

A ce niveau, AdaCore estime que l'IA constitue une technologie puissante permettant aux ingénieurs de travailler avec plus d'efficacité et de pertinence. Loin de remplacer les ingénieurs, l'IA peut automatiser bon nombre des étapes nécessaires à la production de logiciels de haute intégrité, indique la société.

Toutefois, selon AdaCore, l'IA soulève deux défis majeurs pour ce type de développement : d'une part, ses modes de défaillance diffèrent de ceux des humains et sont donc difficiles à prévoir.

D'autre part, elle génère des artefacts à une cadence susceptible de submerger les relecteurs humains.

GNAT Foundry présente ici un flux de travail qui répond à ces enjeux en s'appuyant sur la confiance déterministe délivrée par des outils non basés sur l'IA, agissant comme des garde-fous autour des artefacts générés par l'IA. Les ingénieurs peuvent alors concentrer leur attention là où elle est réellement nécessaire.

Dans ce cadre, l'IA pilote les outils fondés sur le langage Ada SPARK, tandis que ces derniers produisent les preuves de conformité. Ces preuves reposent sur des démonstrations formelles, des résultats de tests fondés sur les exigences, des mesures de couverture structurelle et des données de traçabilité générées par des outils qualifiés et éprouvés.

Plus largement, AdaCore accompagne les projets de logiciels de haute intégrité dans l'utilisation de la suite d'outils Ada SPARK à travers ses logiciels GNAT Pro, SPARK Pro et GNAT DAS.

Selon AdaCore, GNAT Foundry: Intersection illustre une utilisation fiable de l'IA, tant pour des projets open source que propriétaires, pour des projets d’applications à haute intégrité.

« L'IA peut automatiser de nombreuses étapes de la production de logiciels de haute intégrité mais, comme tout projet de développement, elle nécessite un processus outillé pour garantir la fiabilité des résultats obtenus, précise Quentin Ochem, directeur des produits chez AdaCore. Nos outils apportent à ce niveau cette confiance déterministe. Nos outils ayant fait leurs preuves depuis des décennies pour garantir les plus hauts niveaux de qualité logicielle avec des méthodes traditionnelles peuvent désormais être adaptés pour vérifier les artefacts générés par l'IA et fournir des preuves fiables, reproductibles et exploitables. Cela permet d'intégrer dans des logiciels de haute intégrité les artefacts produits par l'IA, qu'il s'agisse de tests, de revues ou même de code. »

Ce démonstrateur est publié sous la forme d'un dépôt public sur Github que les équipes d'ingénierie peuvent cloner et exécuter elles-mêmes.