Logiciels et services pour le développement,
l’analyse et la certification de code embarqué, temps réel et critique.

aiT calcule statiquement des bornes supérieures précises sur les temps d’exécution des tâches de systèmes temps-réel. Ces bornes sont garanties pour tout scénario d’exécution possible. aiT vérifie donc que vos programmes à sûreté critique réagissent toujours en temps voulu.

StackAnalyzer détermine automatiquement l’utilisation au pire cas de la pile des tâches de votre application. Le débordement de pile appartient désormais au passé.

Astrée trouve tous les erreurs à l’exécution dans les codes critiques embarqués écrits en C et peut donc prouver l’absence d’erreurs à l’exécution. Ci-inclus : divisions par zéro, débordements d’index de tableau, mani­pu­lations et déréférences de pointeurs nuls et invalides, débordements arithmétiques, etc.

CompCert est un compilateur C optimisant vérifié formellement. La correction du pro­cessus de compilation est ainsi assurée avec un niveau de confiance sans précédent, contribuant à atteindre les plus hauts niveaux d’assurance du logiciel produit.

Nos analyseurs sont utilisés dans le développement du logiciel de com­mande de vol électrique primaire de plusieurs types d’avion Airbus, dont l’A380, le plus grand avion de transport de passagers du monde.

Notre analyseur des temps d’exécution était utilisé par NASA pour démonstrer l’absence d’erreurs de timing au cours de l’enquête US sur d’accélérations incontrôlées de voitures Toyota.

© AbsInt, image A380 : I. Solt, CC BY-SA 3.0, image Actros © Daimler AG, image prairie : M. Sander, CC BY-SA 3.0. Mentions légales.