AbsInt, l’éditeur allemand d’outils logiciels de développement et de vérification de code à fortes contraintes de sûreté de fonctionnement, a récemment mis à jour l’ensemble de ses logiciels, c'est-à-dire a3 (aiT, TimingProfiler, ...StackAnalyzer, ValueAnalyzer), Astrée et CompCert, avec alignement des mises à jour. AbsInt a notamment intégré au sein d'a3 et d’Astrée (analyse statique de code) la technologie en open source Jenkins qui permet de faire de l’intégration continue, soit la vérification à chaque modification du code source que le résultat de ces changements ne produit pas de régression dans le code applicatif. a3 regroupe les outils phares de la société d’outre-Rhin, à savoir aiT WCET (analyse du comportement temporel d’un programme et du temps d'exécution pire-cas, Worst-Case Execution Time), StackAnalyzer (analyse des débordements de pile pour prévenir les erreurs de runtime) et TimingProfiler (analyse temporelle d’un code embarqué).
Parallèlement, a3 et Astrée bénéficient d’une documentation sur la certification de systèmes médicaux, en phase avec les critères exigés par la FDA aux Etats-Unis. Un document qui s’ajoute à ceux existants, consacrés à la DO-178C pour l’avionique et à l’ISO 26262 pour l’automobile.
Du côté de l’analyseur statique de code Astrée, on notera la détection affinée des interblocages (deadlocks) dans un code, le support de la sémantique des règles Misra très utilisées dans le monde automobile, et la possibilité de réaliser des rapports en HTML.
Cet ensemble d’outils supporte désormais comme cibles les microcontrôleurs MSP430(X) de Texas Instruments et les XMC4500 (à base de Cortex-M4F) d’Infineon.
Enfin, le compilateur CompCert bénéficie d’une interface graphique qui facilite le suivi de la compilation des bibliothèques de runtime sur les cibles embarquées. Rappelons que CompCert est un projet d’origine française piloté par l’Inria sous la houlette de Xavier Leroy. C'est l'un des seuls compilateurs C au monde vérifié de manière formelle par des méthodes mathématiques afin d’assurer la conformité du processus de compilation avec un niveau de confiance très élevé. En d'autres termes, le code produit par le compilateur doit se comporter exactement comme spécifié par la sémantique du programme source C, sans ambiguïté
Les produits d’AbsInt dont CompCert sont distribués en France par Antycip Technologies.
