1. Introduction¶
1.1. CENELEC safety-related railway standards¶
Railway projects are subject to a legal framework (laws, decrees, etc.) and also a normative process based on certification standards. In Europe, these standards are issued and maintained by CENELEC (European Committee for Electrotechnical Standardization). This document explains the usage of AdaCore's technologies in conjunction with EN 50128:2011 [CENELEC11] — Railway applications - Communication, signalling and processing systems - Software for railway control and protection systems — as modified by amendments EN 50128/A1 [CENELEC20a] and EN 50128/A2 [CENELEC20b]. (For ease of exposition, the 2011 edition of the standard, as modified by the A1 and A2 amendments, will simply be referred to as EN 50128.)
EN 50128 is concerned with the safety-related aspects of a railway system, down to the hardware and/or software elements used. This document will cover where AdaCore's technologies fit best and how they can best be applied to meet various requirements in this standard.
EN 50128 is based on fundamentals described in other CENELEC railway standards:
EN 50126-1 [CENELEC17a] — Railway applications - The specification and demonstration of reliability, availability, maintainability and safety (RAMS) - Part 1: Generic RAMS process (subsequently modified by EN 50126-1/A1 [CENELEC24])
EN 50126-2 [CENELEC17b] — Railway applications - The specification and demonstration of reliability, availability, maintainability and safety (RAMS): Part 2: systems approach to safety
EN 50129 [CENELEC18] — Railway applications - Communication, signalling and processing systems - Safety related electronic systems for signalling
As noted in EN 50128, page 7:
EN 50126-1 addresses system issues on the widest scale, while EN 50129 addresses the approval process for individual systems which can exist within the overall railway control and protection system. ... [EN 50128] concentrates on the methods which need to be used in order to provide software which meets the demands of safety integrity which are placed upon it by these wider considerations.
In addition to EN 50126 and EN 50129, several other CENELEC standards relate to software's role in the safety of a railway system:
EN 50657:2017 [CENELEC17c] as modified by amendment EN 50657/A1 [CENELEC23a] — Railways applications - Rolling stock applications - Software on Board Rolling Stock
This standard extends the principles of EN 50128 into the rolling stock domain, focusing on onboard systems such as braking, door control, and driver interfaces.
It retains RAMS goals but tailors them for embedded systems in motion, where environmental and operational variables are more dynamic.
EN 50716:2023 [CENELEC23b] — Railway Applications - Requirements for software development
This standard is a successor to EN 50128 and EN 50657, providing better alignment with EN 50126‑1 and EN 50126‑2. As of 2025 it is at the early adoption stage but is intended to supersede both EN 50128 and EN 50657.
Fig. 4 depicts the relationships among the various standards.
Fig. 4 Relationships among the various standards¶
1.2. Safety Integrity Levels¶
A key concept in EN 50128 is the Safety Integrity Level (SIL) of a software component, which reflects the risk of a hazard occurring if the software fails. If there is no impact on safety, the level is referred to as "Basic Integrity" (earlier known as SIL 0). Otherwise the level has a value between 1 and 4, where 4 is the most critical; i.e., with the highest risk of a hazard in case of software failure.
EN 50128 defines the techniques/measures that need to be used at various software life cycle stages, based on the applicable SIL.
1.3. AdaCore technologies for railway software¶
AdaCore's technologies revolve around programming activities, as well as the closely related design and verification activities. This is the bottom of the "V" cycle as defined in EN 50128, sub-clause 5.3, Figure 4 (see Fig. 5 below). The company's tools exploit the features of the Ada language (highly recommended by table A.15) and its formally verifiable SPARK subset. In particular, the 2012 version of the Ada standard includes some significant capabilities in terms of specification and verification.
AdaCore's technologies bring two main benefits to the software life cycle processes defined by the CENELEC railway standards.
Expressing software interface specifications and software component specifications directly in the source code.
Interfaces can be precisely expressed through standard syntax for features such as strong typing, parameter constraints, and subprogram contracts. These help to clarify interface documentation, to enforce program constraints and invariants, and to provide an extensive foundation for software component and integration verification.
Reducing the verification costs.
Bringing additional specification at the language level allows verification activities to run earlier in the software life cycle, during the software component implementation itself. Tools provided by AdaCore support this effort and are designed to be equally usable by both the development team and the verification team. Allowing developers to use verification tools greatly reduces the number of defects found at the verification stage and thus reduces costs related to change requests identified in the ascending stages of the cycle.
AdaCore's technologies can be used at all Safety Integrity Levels, from Basic Integrity to SIL 4. At lower levels, the full Ada language is suitable, independent of platform. At higher levels, specific subsets will be needed, for example the Ravenscar Profile ([AlanBurnsBDaTVardanega04], [MC15b]) for concurrency support with analyzable semantics and a reduced footprint, or the Light Profile [Adac] for a subset with no run-time library requirements. At the highest level (SIL 4) the SPARK language ([MC15b], [AdaCore and Altran20]) and its verification toolsuite enable mathematical proof of properties including correct information flow, absence of run-time exceptions, and, for the most critical code, correctness of the implementation against a formally defined specification.
The following technologies will be presented:
Ada, a compilable programming language supporting imperative, object-oriented, and functional programming styles and offering strong specification and verification features. Unless otherwise indicated, "Ada" denotes the 2012 version of the Ada language standard.
SPARK, an Ada language subset and toolset supporting formal verification of program properties such as Absence of Run-Time Errors
GNAT Pro Assurance, a specialized edition of AdaCore's GNAT Pro language development environments that is oriented towards projects with long maintenance cycles or certification requirements
The GNAT Static Analysis Suite ("GNAT SAS"), comprising several tools:
A "bug finder" engine that identifies potential defects and vulnerabilities in Ada code
GNATmetric — a metric computation tool
GNATcheck — a coding standard checker
The GNAT Dynamic Analysis Suite ("GNAT DAS"), comprising several tools:
GNATtest — a unit testing framework generator
GNATemulator — a processor emulator
GNATcoverage — a structural code coverage analyzer
GNATfuzz — a fuzzing tool that helps uncover potential faults
TGen — an experimental run-time library for automating test case generation
GNAT Pro for Rust, a professionally supported complete development environment for the Rust programming language
Several Integrated Development Environments (IDEs):
GNAT Studio — a robust, flexible, and extensible IDE
VS Code support — extensions for Ada and SPARK
GNATbench — an Ada-knowlegeable Eclipse plug-in
GNATdashboard — a metric integration and management platform
Fig. 5 Contributions of AdaCore technology to the "V" Cycle¶
Bibliography