Space Technology Special Report - Version B. July 2023 - 19

To maintain efficiency, components communicate with one another, point-to-point, through strongly typed " connectors. " (Image: LASP)
Benefits of Ada
Ada derives its reliability first and
foremost from its strong type system.
In Ada, all types are incompatible by
default. Type conversions are explicit
and only allowed under specific
conditions. Additionally, Ada's types
can be constrained to valid ranges (i.e.,
an integer that can only be assigned
to values between 0 and 10). Variables
are checked against these ranges both
at compile-time and runtime. LASP
engineers found the language to be
strict, but also precise. They changed
their approach to development. By
applying careful thought to the design
of types and abstractions prior to
considering behavior, they were able
to harness the Ada compiler to write
well-defined, defect resistant code.
In Ada, errors that go undetected
during compile time are instead checked
dynamically at runtime. By default,
this includes array index checks and
variable range checks. The language
also allowed LASP engineers to
incorporate custom checking through
" design by contract " mechanisms, such
as preconditions, postconditions, and
predicates. While runtime checks do
impose a small performance penalty,
they can be selectively disabled for highperformance
code sections. These checks
proved invaluable during the creation
of Adamant, as numerous defects were
uncovered early on during development.
Runtime checks are effective but
imagine if these errors could instead
SPACE TECHNOLOGY SPECIAL REPORT
be caught before the code is run. Ada
can be elevated to this next level via
SPARK. SPARK represents a subset of
the Ada language that is specifically
tailored for formal analysis. SPARK
code can be analyzed at different
levels, each offering an increasing
degree of assurance, from guarantees
that code is free of runtime errors to
full verification of the key integrity
properties of a program. LASP
employed this technology to write the
critical boot software for CLARREO.
Not only was the algorithm proven free
of runtime errors, it was also proven
functionally correct, adhering to its
intended design. Interestingly, this was
accomplished by an engineer with
no prior experience in formal proofs,
highlighting the accessibility of SPARK.
The most compelling reason for
choosing Ada as the implementation
language for Adamant is its built-in,
bare metal tasking system. Adamant
requires a priority-preemptive task
scheduler to manage concurrent
operations, but does not need any of
the other extraneous features provided
by common real time operating
systems. In Ada, concurrency is made
possible by the language's firstclass
support for tasking. Whether
operating on Linux or a bare metal
environment, the syntax and semantics
remain the same. The Ada runtime
is lightweight, and for Adamant,
eliminates the need for a separate
RTOS or its associated API calls.
Adamant utilizes runtimes that
adhere to the Ravenscar profile.
This committee-designed standard
limits Ada's tasking facilities to a
subset qualified for safety-critical,
hard real-time computing. The
profile ensures a small memory
footprint and offers efficient,
deterministic execution of tasks,
while eliminating issues such as
deadlock and priority inversion.
Most importantly, the runtime is
manageable in code size, allowing
engineers to fully understand their
entire stack from the bare metal up.
In the domain of spacecraft flight
software, reliability still stands as
an unwavering necessity. Adamant,
with its successful implementation
on CLARREO, exemplifies the pivotal
role that programming language
choice plays in ensuring the success
of a mission. Building on this success,
LASP is proud to release Adamant
open-source on GitHub (https://github.
com/lasp/adamant) later this year. By
embracing an open-source approach,
Adamant opens the doors to wider
collaboration, community contributions,
and the exchange of best practices
in the discipline of flight software.
This article was written by Kevin
Dinkel, Professional Research Assistant,
Laboratory for Atmospheric and
Space Physics, University of Colorado
Boulder. For more information,
visit www.adacore.com.
JULY 2023 19

http://info.hotims.com/85757-23 http://info.hotims.com/85757-23 http://info.hotims.com/85757-24

Space Technology Special Report - Version B. July 2023

Table of Contents for the Digital Edition of Space Technology Special Report - Version B. July 2023