Analyse formelle logicielle renforcée par IA

TrustInSoft fait évoluer son outil TrustInSoft Analyzer avec une version avril 2026 intégrant des fonctionnalités d’intelligence artificielle et des améliorations de ses méthodes formelles. L’objectif est de réduire les coûts d’analyse tout en conservant un niveau de garantie élevé pour les logiciels critiques.
La principale évolution concerne la génération automatisée de stubs et de drivers de test. Grâce à l’IA, ces éléments sont créés de manière contextualisée en un clic, facilitant la mise en place des campagnes de vérification et réduisant le temps de préparation. Cette approche conserve la cohérence exigée par les méthodes formelles tout en améliorant la productivité des équipes.
L’outil introduit également une prise en charge avancée du langage Rust via une interface graphique améliorée. Celle-ci centralise les différentes étapes du workflow : configuration, exécution des analyses, investigation des causes racines et génération de rapports. Cette évolution vise à accompagner l’adoption croissante de Rust dans les systèmes critiques.
Autre point clé, l’analyse de couverture MC/DC bénéficie d’une approche basée sur la généralisation formelle des entrées. Cette méthode permet d’atteindre les exigences de couverture tout en réduisant l’effort de test, notamment dans les contextes normatifs comme l’ISO 26262.
En combinant IA et méthodes formelles, TrustInSoft Analyzer vise à concilier automatisation et preuve mathématique. Cette approche permet de garantir l’absence d’erreurs d’exécution critiques et de défauts de sécurité mémoire dans les codes C, C++ et Rust, avec des applications dans les secteurs de l’automobile, de l’aéronautique, de la défense et de l’IoT.