AdaCore has a long history of providing tools and expertise to the Space industry, helping developers build mission critical applications that extend to the farthest reaches of human exploration.
Space technology is the backbone of modern digital life, helping us to communicate, find our way, monitor the Earth for changes in climate, and literally go where no man has gone before. Still, millions of dollars are spent developing space and satellite projects, and, in most cases, you only get one shot for this kind of application to work, so it is critical to produce safe and totally reliable software.
AdaCore has years of experience working with Space customers and has a deep understanding of the software standards involved and the tools and services needed to ease the workflow and manage costs.
Tools, Runtime Libraries and Qualification Materials
AdaCore tools can be used to meet verification objectives including coding standard compliance, code accuracy (prevention of errors such as buffer overrun, integer overflow, and references to uninitialized variables), and structural coverage analysis up to MC/DC. Specialized high-assurance run-time libraries, including one that implements the Ravenscar tasking profile, are simple enough to be included in qualified systems but expressive enough to support the needed functionality for hard real-time space software. Qualification material for the run-time libraries can be developed for the ECSS standard and adapted to new project contexts.
Sustained Branches
Maintaining qualified software brings unique challenges, since the customer needs to "freeze" on a specific version of the technology for stability, but still might require updated releases if a problem is encountered as the software evolves. AdaCore provides GNAT Pro Assurance subscription which includes a special "sustained branch" service, that supports this requirement
Our Experience with Qualification for Space
AdaCore has extensive experience helping our aerospace customers meet the European Space standards ECSS-E-ST-40C and ECSS-Q-ST-80C. AdaCore has already qualified several versions of the run-time libraries.
ECSS-E-ST-40C and ECSS-Q-ST-80C
The European Cooperation for Space Standardization is an initiative established to develop a coherent, single set of user-friendly standards for use in all European space activities. ECSS-E-ST-40C and ECSS-Q-ST-80C are the software-related standards for use in all European space projects and applications.
Customer Projects: Space
AVIO
AVIO Selects AdaCore’s GNAT Pro Assurance Toolsuite for European Space Agency Program
AVIO has selected the GNAT Pro Assurance Ada Development Environment, including the GNATemulator host-based target emulation tool, to implement the on-board software for AVIO’s Vega-C launch vehicle. Sponsored by the European Space Agency (ESA), this safety-critical hard real-time embedded system is the flight software that handles guidance, navigation and control for the Vega-C.
MDA
MDA Selects AdaCore’s GNAT Pro Assurance Development Platform for International Space Station Software
MDA, a business unit of Maxar Technologies, selected the GNAT Pro Assurance Ada development environment for the LEON3 target processor, to produce the software for a Ku-Band communication subsystem that will replace the current version. This critical International Space Station (ISS) subsystem has to work reliably over the long term, a requirement that led MDA to maintain Ada as the implementation language.
Vermont Technical College
SPARK Going to the Moon
The GNAT Pro and SPARK language toolsets have been selected for the Lunar IceCube project by Vermont Technical College. Lunar IceCube is a 6-Unit CubeSat mission sponsored by NASA through their NextSTEP initiative. The mission will prospect for water and other lunar volatiles in all forms (solid, liquid, and vapor) from a highly elliptical orbit with a low point of 100 kilometers (60 miles) where the data will be gathered, and a high point of 5,000 kilometers (3,100 miles).
Astrium
Astrium Selects AdaCore’s GNAT Pro and PolyORB for International Space Station
Astrium has selected GNAT Pro development environment and PolyORB middleware toolset for use in the Core Ground System (CGS) - CGS forms the basis to operate the Columbus laboratory, the European contribution to the International Space Station (ISS).
Thales
Thales Selects AdaCore Toolset for Argos Satellite Project
The GNAT Pro High Integrity Edition is being used by Thales to develop onboard instrument software for a unique, satellite-based worldwide location and data collection system dedicated to studying and protecting the environment.
Masten Space Systems
How Masten Space Systems is Using Ada and SPARK to Land on the Moon’s South Pole
To develop their mission-critical flight control software, Masten chose the Ada and SPARK programming languages, together with AdaCore’s GNAT Pro integrated development environment and the SPARK Pro static analysis tool suite for their XL-1 Lunar Lander. The lander will transport a suite of scientific research payloads to the lunar south pole.
SEAKR
How to Develop Reliable Spacecraft Systems at Lower Cost with the Ada Programming Language
When SEAKR Engineering decided to upgrade its mission-critical data recorder applications to a new hardware platform, they kept their software in Ada. To help them improve the efficiency and reliability of their Ada code, they upgraded their development environment to GNAT Pro.
GNAT Pro Assurance
GNAT Pro Assurance includes a specialized service known as sustained branches, which allows a project to continue its use of a specific version of the technology, including upgrades to repair critical issues. It supports all versions of the Ada language standard (from Ada 83 to Ada 2012), and C support is an optional add-on. A full toolsuite is supplied, as well as a configurable run-time library and several specific run-times that are especially suited to high-assurance systems.
SPARK Pro
SPARK Pro is a language and toolset specifically designed for developing applications where correct operation is vital for safety or security. The SPARK Pro toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset generates evidence for correctness that can be used to meet the requirements of safety and security certification schemes.
CodePeer
CodePeer is an Ada source code analyzer that detects runtime and logic errors. It assesses potential bugs before program execution, serving as an automated peer reviewer, helping to find errors efficiently and early in the development life-cycle. It can also be used to perform impact analysis when introducing changes to the existing code, as well as helping vulnerability analysis. Using control-flow, data-flow, and other advanced static analysis techniques, CodePeer detects errors that would otherwise only be found through labor-intensive debugging.
GNATcoverage
GNATcoverage allows coverage analysis of both object code (instruction and branch coverage), and Ada or C language source code (Statement, Decision and Modified Condition/Decision Coverage - MC/DC)
QGen
QGen is a model-based development toolsuite for Simulink® and Stateflow® reduces the development and verification costs for developers of safety- and security-critical applications, through qualifiable code generation, model verification, and tight integration with AdaCore’s qualifiable target emulation and structural coverage analysis tools. The QGen code generator can generate MISRA C, but can also generate the verifiable SPARK subset of Ada, from Simulink® and Stateflow®. By selecting SPARK for code generation, can formally prove important safety and security properties of their software, not only enhancing quality but also decreasing testing costs.