Rail - GNAT Pro for Safety-Critical

The GNAT Pro Safety-Critical development environment supports rail applications that need to meet the highest levels of safety certification. It includes run-time libraries specialized for use in safety-critical systems, as well as several tools for static analysis and testing.

GNAT Pro Safety-Critical can be used in conjunction with other AdaCore products such as the SPARK Pro formal verification environment or the CodePeer advanced static analysis tool, providing a unique development framework that supports a wide range of verification activities.

In addition to a fully customizable run-time library, GNAT Pro Safety-Critical supplies several predefined run-time profiles (libraries corresponding to restricted feature choices). The Zero Footprint (ZFP) profile reflects an Ada language subset that does not require any Ada run-time routines, thus reducing the memory footprint to user code only. The Ravenscar Minimal profile implements the Ada Ravenscar tasking subset on top of ZFP. These profiles are intended for high criticality applications, for example, those that need to be certified to Software Safety Integrity Level (SIL) 3/4. For lower levels of criticality, the Ravenscar Extended profile adds features such as exception propagation and stack overflow checking.

GNAT Pro Safety-Critical has been adapted to meet the needs of CENELEC standards for software development processes (EN 50128:2011, EN 50126:1999, and EN 50129:2003, for SIL 3/4), and a variety of certification-related material is available to supplement the product:

  • A SIL 3/4 Independent Safety Assessor (ISA) certificate, confirming the Ravenscar Minimal profile’s conformity to the CENELEC standard
  • Qualification material for several product components:
    • the GNAT Pro compiler as a class T3 tool,
    • the GNATcheck coding standard checker as a class T2 tool,
    • the GNATmetric code metrics generator as a class T2 tool, and
    • the GNATtest / AUnit testing framework as a class T2 tool.

Qualification material is also available for several other tools that can be used in conjunction with GNAT Pro Safety-Critical:

  • SPARK Pro’s GNATprove as a class T2 tool to show proof of absence of run-time errors,
  • the CodePeer static analysis tool as a class T2 tool for data and control flow analysis, and
  • the GNATcoverage and GNATemulator dynamic analysis tools as class T2 tools for code coverage analysis.

Rail Industry Standards

EN 50128

EN-50128 is the European standard used to certify rail applications. It classifies criticality levels between SIL0 (lowest) to SIL4 (highest). Ada is explicitly recommended to reach the highest level of safety (SIL4), as well as other techniques covered by either the GNAT Pro product or companion technologies such as GNATcoverage, SPARK Pro or CodePeer.

Featured Project

Railway Control System by Siemens

The Mobility Division of Siemens Switzerland Ltd., has selected GNAT Pro, along with the CodePeer static analysis tool, to develop the next generation of its railway control and information system.

Featured Book

AdaCore Technologies for CENELEC EN 50128:2011

Learn more about the usage of AdaCore’s technology in conjunction with the CENELEC EN 50128:2011 standard. This book describes where the technology fits best and how it can best be used to meet various requirements of the standard. Written by Jean-Louis Boulanger and Quentin Ochem, for AdaCore.

Download the PDF »

Key Features of GNAT Pro Safety-Critical

  • Configurable Run-Time Library
  • Full Ada 2005 / 2012 Implementation
  • Advanced Static Analysis
  • Simplification of Certification Effort
  • Traceability
  • Safety-Critical Support and Expertise
Learn More »


Knowledge Center


  • When it comes to unmanned aircraft systems (UAS), virtually everyone is talking about and concerned with privacy issues – as though drones were robotic peeping Toms. The much larger and more critical issue, however, is security – without it, the potential exists for control of drones and even swarms of drones to be usurped and used to inflict harm. UAS hardware and software must be designed with development tools proven to be effective in the design and deployment of safety-critical and mission-critical systems and vehicles. In this webinar Robert Dewar will discuss the selection of optimal development tools and processes to ensure the safety, security, and reliability of real-time unmanned aircraft, onboard software, and ground control solutions.
  • The InSight webinar series continues with a webinar demonstrating how to write unit tests in a cost-effective way using the AdaCore toolset. More precisely it will show how to generate the unit testing framework using GNATtest, how to run the tests on an emulator such as GNATemulator and how to extract coverage results using GNATcoverage. This is primary aimed at developers and projects managers that already have unit testing infrastructure in place and are looking to reduce maintenance costs, as well as teams that are looking at implementing such techniques with minimal effort.

Developer Gems    

  • Gem #63: The Effect of Pragma Suppress

    Ada Gem #63 — The features of Ada have generally been designed to prevent violating the properties of data types, enforced either by compile-time rules or, in the case of dynamic properties, by using run-time checks. Ada allows run-time checks to be suppressed, but not with the intent of allowing programmers to subvert the type system.

  • Gem #53: Safe and Secure Software: Chapter 12: Conclusion

    Gem #53 is the concluding chapter of John Barnes' new booklet:

    Safe and Secure Software: An Introduction to Ada 2005.

    We hope you have enjoyed this series. In the attachment at the bottom of Gem #30 you can access the contents and bibliography for the entire booklet.