Safety Critical Products: GMART

A product for statically provable & safe application development

GMART—Green Hills Software’s Minimal Ada Run-Time product—is designed from the ground up to be certifiable to DO-178B Level A, the highest level within the FAA’s commercial avionics safety critical standard. GMART is also designed to support the established safety-critical SPARK language subset. Support for SPARK means that the GMART product is a no run-time, run-time kernel.

SPARK defines a language subset that is fully deterministic as well as statically verifiable to be logically correct. The subset removed those language features that would not be verifiable or are non-deterministic in their behavior. Ada tasking has been completely removed due to the nondeterminism of its full form. For the same reason, protected objects and types have been removed.

Dynamic memory allocation and deallocation have also been removed to avoid run time memory creep and prevent memory fragmentation that may occur in deallocation. To support this restriction, access types are disallowed. General exceptions have been removed since their propagation to a handler can not be statically evaluated. A single global handler is supported to allow for a more graceful system shutdown should an error occur at run time. Generics are disallowed since only physical instances of software modules can be statically proven to be correct.

More easily certified

Although using the SPARK subset removes some generally useful language features, the resulting program is likely simpler and easier to certify to safety critical standards. Removing these language features also allows the Ada Run Time System (RTS) to be simplified and optimized for this subset. Thus the GMART RTS is smaller and faster than general-purpose full Ada RTSes.

Available with INTEGRITY-178

GMART is available as a bare machine Ada RTS or integrated with the INTEGRITY-178 partitioned RTOS. As a bare RTS, GMART provides an extremely small and fast single application execution environment. As a kernel within an INTEGRITY-178 partition, GMART provides all the advantages of the bare model with the added feature of potentially running multiple applications on the same single processor.

A complete safety critical line

Green Hills Software offers a complete safety critical product line that includes:

GMART, GSTART, and INTEGRITY-178 are available with full off-the-shelf DO-178B Level A certification material. All have formally passed DO-178B Level A multiple times as a part of avionics systems and thus are certified and not just certifiable.