Terma A/S has selected the GNAT Pro Safety-Critical Ada development environment for building the onboard software for the Atmosphere-Space Interactions Monitor (ASIM) that will be mounted on the International Space Station.
Terma will use the Adacore GNAT Pro Safety-Critical combined with the GNATemulator and GNATcoverage dynamic testing tools to develop and test the application prior to deployment on the actual LEON 3 embedded processor.
ASIM is used to detect lightning formations known as “red sprites”, “blue jets” and “elves”, and to detect X-ray and gamma-ray discharges. The objective is to search for a correlation between these formations and large thunderstorms, improving understanding of these phenomena and their influence on the Earth’s climate.
Under contract to the European Space Agency (ESA), Terma A/S is the prime contractor for the development of the ASIM instrument including development of the on-board software.
The ASIM will be deployed in space where repairs are costly if possible at all, making reliability of the platform and its software essential. This need for reliability was a principal factor in selecting the Ada programming language for the software development.
The Ravenscar profile (a subset of the Ada tasking features designed for safety-critical hard real-time computing ) will be used to ensure that all multi-processing/tasking within the application can be proven deterministic and schedulable.
Ada’s ability to define static and dynamic contracts and checks – including features recently introduced in the new Ada 2012 standard – helps developers express requirements directly in the software. This allows early detection of inconsistencies, either statically (at compile time) or dynamically (during testing).
To carry out the Ada development, Terma selected the LEON 3 ELF configuration of the GNAT Pro Safety-Critical development environment. It includes tools that take advantage of the language’s properties to perform additional static and dynamic analysis, reaching even higher levels of reliability.
Complexity and other metrics are automatically monitored using GNATmetrics, while GNATcheck enforces a consistent coding style, and detects well-defined categories of code vulnerabilities. The GNATstack tool performs static stack analysis, so that stack size requirements can be verified prior to execution. For dynamic analysis, GNATemulator is used to perform unit testing of the software using the LEON 3 toolchain, independent of and prior to the availability of the final hardware.
In combination with GNATemulator, GNATcoverage is used to provide very early structural coverage analysis without need to instrument the software under test. The software is tested in a fully simulated environment, ensuring that only integration and system-specific verification need to be performed on the final target.