Select Language

AdaCore’s CodePeer Static Analysis Tool Earns Qualification for Software Verification in Avionics, Railway

Automatic code review and validation tool meets rigorous industry software verification standards; provides trusted reliability for Ada developers in safety-critical applications

NEW YORK, PARIS and BRISTOL, October 23, 2014, High Integrity Software Conference, Bristol, UK -- AdaCore today announced that its CodePeer advanced static analysis tool for the automated review and validation of Ada source code has been qualified as a software verification tool for developers in both avionics and railway industries.

CodePeer assesses the program before execution to find errors efficiently and early in the development life cycle. Using advanced mathematics, CodePeer analyzes every line of software, considering every possible input and every path through the program. It performs impact and vulnerability analysis when existing code is modified, and, using control-flow, data-flow and other advanced static analysis techniques, it detects problems that would otherwise require labor-intensive debugging.

“In safety-critical domains, developers need very strong assurances that the tool they’re using to assess their code is reliable, can be trusted, and will substantially reduce the need for manual code review,” says Arnaud Charlet, CodePeer Product Manager and Technical Director at AdaCore. “CodePeer has been through rigorous industry-specific tests for avionics and railway that fully affirm its value and reliability in these and other safety-critical development environments.”

Avionics Qualification
CodePeer has been qualified as a verification tool for DO-178B, the software safety standard for commercial airborne systems. Certification authorities such as the FAA in the U.S. and EASA in Europe apply DO-178B to provide confidence that the software will meet its requirements.

Vulnerabilities detected by CodePeer analysis for avionics include following:

  • Overflow on integer and floating point types
  • Range violations on integer and floating point types
  • Index violations on array operations
  • Division by zero on integer and floating point types
  • Uninitialized variables
  • Underflow on floating point types

Where no potential error is reported, CodePeer guarantees that the code is exempt from these vulnerabilities.

Railway Qualification
For railway applications, CodePeer has been used to verify code certified in accordance with CENELEC EN 50128:2011 SIL 4 --the highest safety integrity level.

In this context, CodePeer has been used for the following activities:

  • Boundary value analysis: it detects attempts to dereference a pointer that could be null, to read values outside the bounds of an Ada type or subtype, and also detects buffer overflows, numeric overflow or wraparound, and division by zero.
  • Control flow analysis: it detects suspicious and potentially incorrect control flows, such as unreachable code, redundant conditionals, loops that either run forever or fail to terminate normally, and subprograms that never return.
  • Data flow analysis: it detects suspicious and potentially incorrect data flows, such as variables read before they are written (uninitialized variables), variables written more than once without being read (redundant assignments), variables that are written but never read, and parameters with an incorrect mode (unread parameter, unassigned parameter).

CodePeer can be used in conjunction with AdaCore’s GNAT Pro development environment where it is tightly integrated into AdaCore’s GPS (GNAT Programming Studio) and GNATbench IDEs, or as a standalone product. It comes with a number of complementary static analysis tools common to the technology: a coding standard verification tool (GNATcheck), a source code metric generator (GNATmetric), a semantic analyzer and a document generator.

A demo highlighting the new features introduced in the latest version of CodePeer can be viewed at the following url: http://www.adacore.com/codepeer-2-3-demo/

About AdaCore
Founded in 1994, AdaCore is the leading provider of commercial software solutions for Ada, a state-of-the-art programming language designed for large, long-lived applications where safety, security, and reliability are critical. AdaCore's flagship product is the open source GNAT Pro development environment, which comes with expert on-line support and is available on more platforms than any other Ada technology. AdaCore has an extensive world-wide customer base; see www.adacore.com/customers/ for further information.

Ada and GNAT Pro see a growing usage in high-integrity and safety-certified applications, including space-based systems, commercial aircraft avionics, military systems, air traffic management/control, railroad systems, and medical devices, and in security-sensitive domains, such as financial services. The SPARK Pro toolset, available from AdaCore, is especially useful in such contexts.

AdaCore has North American headquarters in New York and European headquarters in Paris. www.adacore.com

Press Contacts

Jamie Ayre

AdaCore

press@adacore.com

http://twitter.com/AdaCoreCompany

Jenna Beaucage
Rainier Communications
jbeaucage@rainierco.com
508.475.0025, ext. 124

CodePeer, l’outil d’analyse statique développé par AdaCore, certifié pour la vérification de code dans les domaines aéronautique et ferroviaire

L’outil de validation automatique de code a passé avec succès les tests les plus rigoureux de l’industrie du logiciel de vérification et représente un outil fiable pour les développeurs d’applications critiques en langage Ada

NEW YORK, PARIS et BRISTOL, le 23 octobre 2014, High Integrity Software Conference, Bristol, UK – AdaCore a aujourd’hui annoncé que l'outil d'analyse statique CodePeer pour la revue et validation de code source Ada a été qualifié comme outil logiciel de vérification pour le développement de logiciels à destination des industries de l’aéronautique et du ferroviaire.

CodePeer évalue un programme avant exécution et permet ainsi une recherche en amont et efficace d’erreurs de codage. Basé sur des outils mathématiques de haut niveau, CodePeer analyse chaque ligne de code en prenant en compte toutes les entrées possibles ainsi que tous les retours à l’intérieur du programme. A chaque modification du code, il évalue son impact sur les vulnérabilités du programme, et à l’aide d’outils techniques d’analyse statique avancée tels que l’analyze du flux de contrôle et de de données, il détecte des problèmes qui auraient nécessités un long travail de débogage.
“Dans les domaines où la sureté représente un enjeu important, il est nécessaire pour les développeurs d’avoir des garanties sur fiabilité des outils de vérification de code, afin de savoir qu’ils peuvent leur faire confiance pour réduire les revues manuelles”, précise Arnaud Charlet, responsable du projet CodePeer et directeur technique chez AdaCore. “CodePeer a été soumis avec la plus grande rigueur à des tests spécifiques à l’aéronautique et au ferroviaire. Ceux-ci valident pleinement son efficacité et sa fiabilité dans ces domaines, et par conséquent dans l’ensemble des environnements où la sureté est cruciale.”

Certification aéronautique
CodePeer a été qualifié comme outil de vérification suivant la norme DO-178B, un standard pour le développement de logiciels dans le domaine aéronautique. Les agences gouvernementales de certification s’appuient sur la norme DO-178B pour prouver l’intégrité de certains logiciels; c’est la cas par exemple de la FAA aux Etats-Unis et de la EASA en Europe.

Parmi les points de vulnérabilité aéronautique détectés par CodePeer, on trouve les suivants:

  • Débordement sur les variables de type entier ou flottant (overflow)
  • Dépassement de capacité pour les entiers et flottants
  • Dépassement de capacité lors d’opérations sur des tableaux (buffer overflow)
  • Division par zéro pour les entiers et les flottants
  • Variables non initialisées
  • Soupassement de capacité en virgule flottante (underflow)

Dans le cas où CodePeer ne détecte aucune erreur, le développeur a la garantie que son code n’en contient aucune parmi celles citées dans cette liste.

Certification ferroviaire
En ce qui concerne les applications pour le ferroviaire, CodePeer s’est avéré remplir toutes les exigences de la norme CENELEC EN 50128:2011 SIL 4, qui représente le plus haut niveau de sécurité en matière d’intégrité du code. CodePeer a été qualifié en tant qu’outil de classe T2.

Dans ce cadre, CodePeer a été utilisé pour les activités suivantes:

  • L’analyse des valeurs limites: CodePeer détecte les tentatives de déréférencement de pointeurs potentiellement nuls, les lectures de valeurs numériques hors des limites que son type permet, mais également le débordement de mémoire tampon, le débordement numérique, et les divisions par zéro
  • L’analyse de la structure de contrôle: CodePeer détecte les enchaînements d’instructions suspects et potentiellement incorrects, comme un code inaccessible, les tests de condition redondants, des boucles infinies ou qui pourraient mal se terminer, et les sous-programmes qui ne renvoient aucune valeur
  • L’analyse des flux de données: il détecte les flux suspects et potentiellement incorrects, comme les variables lues avant d’être initialisées, les variables assignées plusieurs fois sans être lues, les variables initialisées mais jamais utilisées, et les paramètres en mode incorrect (non initialisés ou non utilisés).


CodePeer peut être utilisé de manière conjointe avec l’environnement de développement GNAT Pro d’AdaCore, ou bien comme programme autonome. Il est en effet adapté au GPS d’AdaCore (GNAT Programming Studio) et aux bancs d’essais des environnement de développement logiciel GNAT. Il apporte un certain nombre d’outils complémentaires d’analyse statique à ces technologies existantes: un outil de vérification de code (GNATcheck), un générateur de métriques de code source (GNATmetric), un analyseur sémantique et un générateur de document.

A propos d’AdaCore
AdaCore, fondé en 1994, est le premier fournisseur de solutions logicielles commerciales pour Ada, un langage de programmation de pointe conçu pour des applications de grande taille et à grande durée de vie. Les technologies fournies par AdaCore sont particulièrement adaptées aux applications pour lesquelles la sûreté, la sécurité et la fiabilité sont des éléments critiques.  Le produit phare d'AdaCore est l'environnement de développement GNAT Pro, disponible sur le plus vaste ensemble de plateformes de toutes les technologies Ada. Il est fourni avec un support en ligne dispensé par des experts parmi les plus reconnus dans le domaine.  AdaCore dispose d’une large base de clients située dans le monde entier ; voir http://www.adacore.com/home/company/customers/ pour de plus amples informations.

L'utilisation d'Ada et de GNAT Pro connaît une croissance continue dans les applications critiques ou certifiées pour la sûreté, comme les éléments d'avionique pour les appareils commerciaux, les systèmes militaires, le contrôle aérien, les systèmes ferroviaires, les appareils médicaux, et dans des domaines sensibles pour la sécurité comme les services financiers.

Le siège social d’AdaCore est situé à Paris pour la zone Europe, et à New York pour la zone Amérique du Nord. http://www.adacore.com

Jamie Ayre

AdaCore

press@adacore.com

http://twitter.com/AdaCoreCompany

Jenna Beaucage
Rainier Communications
jbeaucage@rainierco.com
508.475.0025, ext. 124