Safety Critical Products: GMART

A complete safety critical line
GMART definition
  • No tasks other than the environment task
  • No protected objects
  • Compiler support routines (such as block moves)
  • User-selectable exception handling (single handler or propagation)
  • No generics
    (user selectable)
  • No exceptions
    (user selectable)
  • No memory allocation or deallocation

 Key Customers           
- Lockheed Martin
- Boeing
- Rockwell
- Raytheon
- BAE SYSTEMS
- BF Goodrich Aerospace
- Alenia Aerospatiale

- Project Details
           

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

GMART, GSTART, and INTEGRITY-178B 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.

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-178B

GMART Ada Run-Time Systems for DO-178B, MILS-Compliant, EAL 6+ Safety Critical Software, ARINC-653-1 - Green Hills Software

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

© 1996-2017 Green Hills Software Trademark & Patent Notice