What is EN 50128?
EN 50128 is a certification standard issued by CENELEC (the European Committee for Electrotechnical Standardization). It "specifies the process and technical requirements for the development of software for programmable electronic systems for use in railway control and protection applications". Together with EN 50126 and EN 50129, the EN 50128 standard defines certain objectives in terms of Reliability, Availability, Maintainability and Safety. The scope of these standards is summarized in the following figure:
EN 50128 defines five software safety integrity levels, from SIL 0 (lowest) to SIL 4 (highest), and specifies a variety of techniques and measures that support sound software engineering throughout the software life cycle. The standard identifies whether the techniques and measures are recommended, or highly recommended, based on the SIL. For example Formal Methods are highly recommended at SIL 3 and SIL 4; Static Analysis is highly recommended at SIL 1 through SIL 4; the Ada programming language is highly recommended at SIL 1 through SIl 4 (and is recommended at SIL 0); the C and C++ languages are recommended, but not highly recommended, at SIL 0 through SIL 4.
One of the major contributions in the 2011 version of EN 50128 is the specification of the requirements for tool qualification. Three classes of tools are defined: T1, T2 and T3. The T1 class applies to tools that affect neither the verification nor the final executable. T2 applies to tools where a fault could lead to an error in the results of verification or validation. An example of a T2 tool is a coding standard checker. T3 applies to tools which, if faulty, could introduce errors into the final executable (for example a compiler).
AdaCore's technology can be used at all levels, from Sil 0 through SIL 4. At lower levels the full Ada language is suitable; at higher levels specific subsets will be needed (for example the Ravenscar profile which provides a safe and efficient set of concurrency features, or the Zero Footprint Profile with no run-time library requirements). At the highest level the SPARK technology can provide mathematics-based assurance of program properties such as absence of run-time errors.
A number of AdaCore tools have been qualified at T2 and T3. These include The GNAT Pro Ada compiler at T3 and CodePeer, GNATcheck, GNATcoverage and SPARK Pro at T2.
Read our booklet on CENELEC EN 50128:2011
This document presents the usage of AdaCore’s technology in conjunction with the CENELEC EN 50128:2011 standard. It 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.
GNAT Pro Assurance
GNAT Pro Assurance includes a specialized service known as sustained branches, which allows a project to continue its use of a specific version of the technology, including upgrades to repair critical issues. It supports all versions of the Ada language standard (from Ada 83 to Ada 2012), and C support is an optional add-on. A full toolsuite is supplied, as well as a configurable run-time library and several specific run-times that are especially suited to high-assurance systems.