Avec la version 26.10 de son logiciel de test TrustInSoft Analyzer - TISA -  la société française TrusInSoft, fournisseur de solutions de vérification logicielle à garanties mathématiques, introduit la notion d’automatisation assistée par l’intelligence artificielle (IA) afin de réduire l’effort d’ingénierie nécessaire à la mise en place de l’analyse formelle.

Dans cette version 2026, le logicele TISA propose également des fonctionnalités améliorées de couverture MC/DC (Modified Condition/Decision Coverage), conçues pour aider les équipes développant des logiciels critiques pour la sécurité à atteindre une couverture complète en moins d’étapes.

« Avec TISA 26.10, nous associons la puissance de l’automatisation par l’IA à la rigueur de la vérification formelle afin de rendre la vérification logicielle exhaustive plus rapide et plus facile à déployer à grande échelle, commente Caroline Guillaume, CEO de TrustInSoft. L’IA automatise le travail d’ingénierie nécessaire à la mise en place de l’analyse, tandis que TrustInSoft Analyzer fournit les garanties mathématiques, permettant aux équipes de vérifier davantage les codes écrits en C, C++ et Rust avec nettement moins d’efforts manuels. »

Concrètement, les équipes d’ingénierie peuvent désormais utiliser un agent de codage fondé sur l’IA pour automatiser les principales étapes nécessaires à la préparation et à la configuration d’une campagne d’analyse, tout en suivant sa progression et en consultant les résultats directement dans le logiciel TISA.

A ce niveau, l’IA facilite le travail d’ingénierie lié à l’analyse alors que TrustInSoft Analyzer se charge quant à lui de la vérification proprement dite. Son analyse formelle explore les comportements possibles dans le périmètre d’analyse et selon les hypothèses définies, fournit des garanties mathématiques quant à l’absence de classes ciblées d’erreurs d’exécution et de comportements indéfinis.

Cette séparation associe la productivité de l’IA à la rigueur et à l’"auditabilité" des méthodes formelles, estime TrusInSoft. En réduisant les tâches répétitives de mise en place et de configuration, les équipes peuvent ainsi obtenir plus rapidement, selon TrusInSoft, des résultats de vérification et appliquer une analyse exhaustive à des parties plus importantes de leur logiciel.

Quant à la couverture MC/DC, TISA 26.10 permet d’atteindre une couverture complète en moins d’étapes que précédemment grâce à un niveau d'automatisation accru, afin d’aider les équipes à identifier et à combler plus efficacement les lacunes de couverture, et à générer des rapports axés sur la certification ainsi qu'une traçabilité.

Plutôt que de construire la couverture test par test, TrustInSoft Analyzer propose d’utiliser l’analyse formelle pour raisonner sur des plages de valeurs d’entrée possibles au cours d’une seule analyse. La vue sous forme de table de vérité qui en résulte montre quelles combinaisons contribuant à la couverture MC/DC ont été couvertes et lesquelles restent à atteindre.

Chaque combinaison accessible signalée correspond à une exécution réalisable du programme. Lorsque des lacunes subsistent, les ingénieurs peuvent concentrer des analyses supplémentaires spécifiquement sur les conditions manquantes, plutôt que de construire la couverture de manière itérative, test par test.

Le résultat est une approche plus systématique pour atteindre une couverture MC/DC complète, avec des rapports détaillés et une traçabilité permettant de soutenir les activités de vérification.

Une manière de faire jugée particulièrement pertinente par TrusInSoft, pour les équipes développant des logiciels critiques pour la sécurité qui travaillent conformément à des normes telles que l’ISO 26262 ASIL D dans l'automobile.