![]() |
| Safety Critical Products: GMART | |||||||||||||||||||||
| » Download GMART datasheet (PDF) | |||||||||||||||||||||
| A complete safety critical line | |||||||||||||||||||||
|
|
|||||||||||||||||||||
|
Green Hills Software offers a complete safety critical product line that includes:
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.
GMART is available as a bare machine Ada RTS or integrated with the INTEGRITY-178B partitioned RTOS. As a bare RTS, GMART provides an extremely small and fast single application execution environment. As a kernel within an INTEGRITY-178B partition, GMART provides all the advantages of the bare model with the added feature of potentially running multiple applications on the same single processor. |
|||||||||||||||||||||
|
|||||||||||||||||||||
|
Safety Critical Products: INTEGRITY - High Reliability RTOS Solution INTEGRITY-178B - DO-178B Level A Safety Critical Certified RTOS MULTI - Advanced Multi-Language Development Environment AdaMULTI - Ada Enabled Advanced Multi-Language Development Environment GMART - DO-178B Level A SPARK Compliant Safety Critical kernel GSTART - DO-178B Level A Ravenscar Compliant Safety Critical kernel G-Cover - DO-178B Level A Qualified Test Capability | |||||||||||||||||||||
|
|