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 ou 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.

Depuis deux décennies, Airbus France utilise nos analyseurs 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.

aiT, StackAnalyzer et ValueAnalyzer ont été utilisés avec succès par Honda dans le développement logiciel FADEC d’une turbosoufflante d’avion.

Daimler utilise aiT et StackAnalyzer pour de nombreux logiciels automobiles, notamment le système de contrôle du groupe motopropulseur du nouveau camion Actros.

aiT é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.

Le fournisseur automobile global Helbako utilise Astrée dans le processus de développement pour démontrer la conformité du code avec MISRA et pour vérifier qu’aucune erreur à l’exécution ne peut arriver dans les logiciels de contròle électronique.

Astrée et RuleChecker sont déployés par l’équipementier automobile Robert Bosch, après une expérimentation intensive d’un an dans sa Division « Automotive Steering ».

OHB utilise aiT et StackAnalyzer dans le développement de logiciel embarqué essentiel pour le succès des missions de la plateforme satellite SmallGEO pour les satellites de communication géostationnaire et la plateforme GALILEO FOC pour la localisation par satellite.

Astrée pouvait prouver l’absence de tout erreur d’exécution dans une version C des logiciels d’accostage automatique du Véhicule automatique de transfert européen (ATV) Jules Verne développé pour ravitailler la Station spatiale internationale (ISS). L’analyse était effectuée de façon complètement automatique.

MTU Friedrichshafen utilise aiT, StackAnalyzer et Astrée pour démontrer la justesse du logiciel de contrôle pour les générateurs de secours dans les centrales électriques. Les outils combinés avec leurs kits de qualification (QSK et QSLCD) font partie du processus de certification selon l’IEC60880.

Depuis 2000, nous avons collaboré avec le Commissariat à l’énergie atomique et aux énergies alternatives sur de nombreux projets de recherche de l’UE.

U-blox en Suisse, premier fournisseur mondial de communication embarquée sans fil et de solutions de déploiement, utilise StackAnalyzer afin d’éviter les problèmes de dépassement de pile au moment de compiler et pour augmenter la fiabilité et la qualité de nos logiciels de contròle.