Software development and verification tools and expertise for mission-critical, safety-critical, and security-critical systems.
AdaCore provides open source tools and expertise for the development of mission-critical, safety-critical, and security-critical software. AdaCore’s flagship products are the GNAT Pro and SPARK Pro development environments and the CodePeer automatic code reviewer and validator. Customers around the world, including major actors in the domains of commercial aircraft avionics, military systems, air traffic management/control, railroad systems, medical devices, and financial services, trust GNAT Pro and AdaCore.
AdaCore supplies software development and verification tools, and expertise to help organizations build mission-critical, safety-critical, and security-critical systems. Four flagship products highlight our 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 before they get into your 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.
These tools help reduce your team’s development and verification costs by leveraging Ada’s software engineering benefits and, in the case of QGen, by ensuring traceability from the model to readable generated source code.
Over the years customers have used AdaCore products to field and maintain a wide range of applications, including safety-critical systems consisting of millions of lines of code and requiring certification at the highest levels. Our technology is continually enhanced, with annual product releases issued on dozens of platforms and backed by unmatched support services to address customer questions.
Customers around the world, including major commercial and government organizations from domains such as aircraft avionics, military systems, air traffic management/control, space, rail systems, medical devices, and financial services, rely on AdaCore products. Companies using AdaCore tools and services include Airbus Group, Alstom, Ansaldo STS, BAE Systems, BNP Paribas, Boeing, Embraer, Eurocontrol, GE Avionics, General Dynamics, Honeywell, L-3 Communications, Lockheed Martin, MBDA, Mitsubishi, PostFinance, Raytheon, Rockwell Collins, Rolls-Royce, Saab, Siemens, Sikorsky, Thales, and UTC Aerospace Systems.
Development and Verification Tools
AdaCore's tools are targeted to applications with demanding requirements for high reliability, safety/security, and maintainability.
- The GNAT Pro Ada development environment provides tools that can compute code metrics, demonstrate compliance with coding standards, calculate maximum stack usage, and perform other functions that assist verification. The GNAT technology implements all versions of the Ada standard from Ada 83 through Ada 2012 and includes Integrated Development Environments – the GNAT Programming Studio (GPS) and the GNATbench Eclipse plug-in – that support large and long-lived software systems.
- The CodePeer advanced static analysis tool exploits Ada’s software engineering support to identify run-time vulnerabilities in both existing code and software under development. It analyzes programs for a wide range of flaws including use of uninitialized data, pointer misuse, buffer overflow, numeric overflow, division by zero, unreachable code, and concurrency faults (race conditions).
- SPARK Pro analyzes programs in the SPARK subset of Ada, using formal methods to prove program properties ranging from absence of run-time errors to compliance with formally specified requirements. The SPARK technology has been upgraded to implement SPARK 2014, which complies with Ada 2012 syntax for contracts, and it supports “hybrid verification” that combines formal methods with traditional techniques based on testing.
- AdaCore's dynamic analysis technologies for emulation, unit testing, and code coverage verification help reduce the effort for software development, quality assurance, and official certification against safety or security standards.
- At a higher level of abstraction, the QGen tool supports model-based development for safety-critical software through a qualifiable code generator and model verifier for Simulink® and Stateflow® models. QGen can be used to show that the model and the generated source code behave the same, and that the generated code complies with the relevant safety standard. QGen can generate code for both SPARK and MISRA C.
Expertise / Support / Training
At the heart of every AdaCore subscription are the consulting and support services we provide to our customers. AdaCore staff are internationally recognized experts on the Ada language, software certification standards, compilation technologies, and static and dynamic verification techniques. They have extensive experience in helping customers use our products to develop critical systems. Every AdaCore subscription comes with first-hand support provided directly by these experts, who are also the developers of the technology. Customers’ questions (requests for guidance, technology enhancements, or problem reports) are handled promptly and effectively.
In addition to this bundled support, AdaCore offers Ada language and tools training, as well as on-site consulting for specialized assistance with customer projects. On-demand tool development, product ports to new platforms, and tool qualification services are also available.
Safety / Security / Certification
Customers have used AdaCore products to develop software that has to meet the highest levels of safety standards such as DO-178B and DO-178C (avionics), EN 50128 (railway), ECSS-E-40/ECSS-Q-80 (space), and DEF STAN 00-55/56 (UK military). We have extensive experience with safety certification, and AdaCore personnel have participated actively in the definition of the DO-178C standard and its supplements.
A range of tools, certification material and qualification packages are available to support the highest levels of safety certification:
- Qualified Code Standard Checker
- Qualifiable Code Coverage Analyzer
- Source-to-Object Code Traceability Analysis Package
- CodePeer Deep Static Analysis Tool
- Certifiable Run-Time Libraries
- A specialized subscription option (sustained branches) for customers who need access to defect corrections that were implemented on defined release branches
In the security arena the SPARK Pro product is especially applicable. The SPARK language has been used in systems that need to satisfy the most stringent security requirements, achieving ultra-high reliability through formal methods at a level of effort no greater than for conventional software projects.
46, rue d`Amsterdam
Tel: +33 14970-6716
Fax: +33 14970-0552