GNAT Pro Safety-Critical used by Terma A/S for Space Monitor Project

ASIM is used to detect lightning formations known as “red sprites”, “blue jets” and “elves”, and to detect X-ray and γ-ray discharges. The objective is to search for a correlation between these formations and large thunderstorms, improving our understanding of these phenomena and their influence on the Earth’s climate. Terma is – under contract to the European Space Agency (ESA) – the prime contractor for the development of the ASIM instrument including development of the on-board software.

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.

“At Terma we find Ada to be suitable for on-board software development, due to its strengths and proven track record in the field of critical real-time software. By choosing GNAT Pro for LEON 3 ELF, we have an Ada development toolchain that can deliver the required quality, and body of evidence thereof, needed when developing critical software. We are excited about not having to rely on a separate real-time operating system, as GNAT Pro for LEON 3 ELF allows us to develop Ravenscar-compliant real-time software targeting a LEON 3 bare-board with a minimum of fuss.” [Mark Lorenzen, Software Engineer, ASIM instrument software responsible]

“Ada and GNAT Pro have a solid track record in space applications, and their selection for the ASIM software continues to demonstrate their advantages in this critical domain.” said Cyrille Comar, Managing Director at AdaCore. “What is particularly pleasing in this project is to see Terma using the full range of complementary technologies that make up GNAT Pro to ensure the highest levels of reliability.”