AdaCore’s CodePeer Selected for Digital Terrain System Requiring DO-178B Certification
Static analysis tool to be qualified as DO-178B verification tool, reducing software certification costs for industry leader UTC Aerospace Systems
NEW YORK and PARIS, January 27, 2016 - AdaCore today announced that its CodePeer static analysis tool has been adopted by Atlantic Inertial Systems Limited, a UTC Aerospace Systems company in the U.K., for usage on its TERPROM® digital terrain system for military transport aircraft. CodePeer automates the review and validation of Ada source code and helps detect potential errors early in development. As a qualified tool that automates several verification activities, CodePeer will facilitate UTC Aerospace Systems’ DO-178B certification of the TERPROM terrain referenced navigation software–the software that allows the TERPROM system to provide precise, reliable and predictive ground proximity warnings.
The CodePeer tool is sound; that is, it does not report false negatives. If CodePeer’s analysis of a program module reports no errors of a given type, then no errors are present. The static analysis tool reduces the need for manual code review, provides deep insight into potential issues, and automates parts of the DO-178B verification process for the certification of software in airborne systems. According to Hugh Williams, engineering director at UTC Aerospace Systems in Plymouth, “this analysis tool should help improve computational accuracy and verify that code is free of certain categories of run-time errors such as buffer overflows, floating point underflows and overflows, integer overflows and references to uninitialized variables.”
“Sound static analyzers allow code reviews to be significantly more effective and less time consuming than traditional manual methods,” said Cyrille Comar, AdaCore President and a member of the SC205 (DO-178C) Working Group . “This automation is a major new trend in the verification of critical software, and we are pleased to lend our support by qualifying CodePeer for our avionics customers.”
About UTC Aerospace Systems
UTC Aerospace Systems is one of the world’s largest suppliers of technologically advanced aerospace and defense products. It designs, manufactures and services systems and components and provides integrated solutions for commercial, regional, business and military aircraft, helicopters and other platforms. It is also a major supplier to international space programs.
Serving as an efficient and accurate code reviewer, CodePeer identifies constructs that are likely to lead to run-time errors such as buffer overflows, and it flags legal but suspect code, typical of logic errors. Going well beyond the capabilities of typical static analysis tools, CodePeer also produces a detailed analysis of each subprogram, including pre- and post-conditions. Such an analysis makes it easier to find potential bugs and vulnerabilities early: if the implicit specification deduced by CodePeer does not match the component’s requirements, a reviewer is alerted immediately to a likely logic error. During system development, CodePeer can help prevent errors from being introduced, and it can also be used as part of a systematic code review process to dramatically increase the efficiency of human review. Furthermore, CodePeer can be used retrospectively on existing code, to detect and remove latent bugs.
CodePeer has been previously qualified as a verification tool under DO-178B on other airborne systems, and it has also been qualified as a class T2 tool for data and control flow analysis under EN 50128 for rail systems.
Founded in 1994, AdaCore supplies software development and verification tools for mission-critical, safety-critical, and security-critical systems. Four flagship products highlight the company’s offerings:
- The GNAT Pro development environment for Ada, a complete toolset for designing, implementing, and managing applications that demand high reliability and maintainability,
- The CodePeer advanced static analysis tool, an automatic Ada code reviewer and validator that can detect and eliminate errors both during development and retrospectively on existing software,
- The SPARK Pro verification environment, a toolset based on formal methods and oriented towards high-assurance systems, and
- The QGen model-based development tool, a qualifiable and customizable code generator and verifier for Simulink® and Stateflow® models, intended for safety-critical control systems.
Over the years customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as space systems, commercial avionics, military systems, air traffic management/control, rail systems, medical devices, and financial services. AdaCore has an extensive and growing world-wide customer base; see www.adacore.com/customers/ for further information.
AdaCore products are open source and come with expert on-line support provided by the developers themselves. The company has North American headquarters in New York and European headquarters in Paris. www.adacore.com
Rainier Communications (for AdaCore)
Tel: +1-508-475-0025 x124