AdaCore Technologies for Railway Software

Supporting certification for CENELEC 50128

Download PDF Download EPUB

About the Authors

Jean-Louis Boulanger

Since the late 1990s Jean-Louis Boulanger has been an independent safety assessor for the CERTIFER certification authority in France, for safety-critical software in railway systems. He is an experienced safety expert in both the railway industries with the CENELEC standard and the automotive domain with ISO 26262. He has published a number of books on the industrial use of formal methods, as well as a book on safety for hardware architectures and a recent book on the application of the CENELEC EN 50128 and IEC 62279 standards. He has also served as a professor and researcher at the University of Technology of Compiègne.

Quentin Ochem

Quentin Ochem is the Chief Product and Revenue Officer at AdaCore, where he oversees marketing, sales, and product management while steering the company's strategic initiatives. He joined AdaCore in 2005 to work on the company's Integrated Development Environments and cross-language bindings. With an extensive background in software engineering in high-integrity domains such as avionics and defense, he has served leading roles in technical sales, customer training, and product development. Notably, he has conducted training on the Ada language, AdaCore tools, and the DO ‑ 178B/ED ‑ 12B and DO ‑ 178C/ED ‑ 12C software certification standards. In 2021 he stepped into his current role, directing the company's strategic initiatives.

Foreword

The guidance in the CENELEC standard EN 50128:2011 helps achieve confidence that railway control and protection software meets its safety requirements. Certifying compliance with this standard is a challenging task, especially for the testing and verification activities, but appropriate usage of qualified tools and specialized run-time libraries can significantly simplify the effort. This document explains how a number of technologies offered by AdaCore — tools, libraries, and supplemental services — can help. The content is based on the authors' many years of practical experience with the certification of railway software and with the Ada and SPARK programming languages.

Jean-Louis Boulanger

October 2015

Quentin Ochem, AdaCore

October 2015

Foreword to V2.1

In the years since the initial version of this document was published, the EN 50128:2011 standard has been amended twice, and AdaCore's products have evolved to meet the growing demands for, and challenges to, high assurance in mission-critical real-time software. This revised edition reflects the current (2025) versions of EN 50128 and AdaCore's offerings. Among other updates and enhancements to the company's products, the static analysis tools supplementing the GNAT Pro development environment have been integrated into a cohesive toolset (the GNAT Static Analysis Suite). The dynamic analysis tools have likewise been consolidated, and the resulting GNAT Dynamic Analysis Suite has introduced a fuzzing tool — GNATfuzz — which exercises the software with invalid input and checks for failsafe behavior.

As editor of this revised edition, I would like to thank Vasiliy Fofanov (AdaCore) for his detailed and helpful review and suggestions.

For up-to-date information on AdaCore support for developers of rail software, please visit [Adab].

Ben Brosgol, AdaCore

September 2025

• 1. Introduction
  • 1.1. CENELEC safety-related railway standards
  • 1.2. Safety Integrity Levels
  • 1.3. AdaCore technologies for railway software
• 2. CENELEC EN 50128
  • 2.1. Overview
  • 2.2. Structure of the standard
  • 2.3. Tool qualification
    • 2.3.1. Tool classes
    • 2.3.2. AdaCore tool qualification support
• 3. Tools and Technologies Overview
  • 3.1. Ada
    • 3.1.1. Background
    • 3.1.2. Language Overview
      • 3.1.2.1. Scalar Ranges
      • 3.1.2.2. Contract-Based Programming
      • 3.1.2.3. Programming in the large
      • 3.1.2.4. Generic Templates
      • 3.1.2.5. Object-Oriented Programming (OOP)
      • 3.1.2.6. Concurrent Programming
      • 3.1.2.7. Systems Programming
      • 3.1.2.8. Real-Time Programming
      • 3.1.2.9. High-Integrity Systems
      • 3.1.2.10. Summary
  • 3.2. SPARK
    • 3.2.1. Flexibility
    • 3.2.2. Powerful Static Verification
    • 3.2.3. Ease of Adoption
    • 3.2.4. Hybrid Verification
    • 3.2.5. Reduced Cost and Improved Efficiency of Executable Object Code Verification
  • 3.3. GNAT Pro Assurance
    • 3.3.1. Sustained Branches
    • 3.3.2. Language and Tool Support
    • 3.3.3. Configurable Run-Time Libraries
    • 3.3.4. Full Implementation of Ada Standards
    • 3.3.5. Source to Object Traceability
    • 3.3.6. Safety-Critical Support and Expertise
    • 3.3.7. Libadalang
    • 3.3.8. GNATstack
  • 3.4. GNAT Static Analysis Suite (GNAT SAS)
    • 3.4.1. Defects and Vulnerability Analyzer
    • 3.4.2. GNATmetric
    • 3.4.3. GNATcheck
  • 3.5. GNAT Dynamic Analysis Suite (GNAT DAS)
    • 3.5.1. GNATtest
    • 3.5.2. GNATemulator
    • 3.5.3. GNATcoverage
    • 3.5.4. GNATfuzz
    • 3.5.5. TGen
  • 3.6. GNAT Pro for Rust
  • 3.7. Integrated Development Environments (IDEs)
    • 3.7.1. GNAT Studio
    • 3.7.2. VS Code Extensions for Ada and SPARK
    • 3.7.3. Eclipse Support – GNATbench
    • 3.7.4. GNATdashboard
• 4. AdaCore Contributions to The Software Quality Assurance Plan
  • 4.1. Table A.3 – Software Architecture (7.3)
  • 4.2. Table A.4 – Software Design and Implementation (7.4)
  • 4.3. Table A.5 – Verification and Testing (6.2 and 7.3)
  • 4.4. Table A.6 – Integration (7.6)
  • 4.5. Table A.7 – Overall Software Testing (6.2 and 7.7)
  • 4.6. Table A.8 – Software Analysis Techniques (6.3)
  • 4.7. Table A.9 – Software Quality Assurance (6.5)
  • 4.8. Table A.10 – Software Maintenance (9.2)
  • 4.9. Table A.11 – Data Preparation Techniques (8.4)
  • 4.10. Table A.12 – Coding Standards
  • 4.11. Table A.13 – Dynamic Analysis and Testing
  • 4.12. Table A.14 – Functional/Black Box Test
  • 4.13. Table A.15 – Textual Programming Language
  • 4.14. Table A.17 – Modeling
  • 4.15. Table A.18 – Performance Testing
  • 4.16. Table A.19 – Static Analysis
  • 4.17. Table A.20 – Components
  • 4.18. Table A.21 – Test Coverage for Code
  • 4.19. Table A.22 – Object Oriented Software Architecture
  • 4.20. Table A.23 – Object Oriented Detailed Design
• 5. Technology Usage Guide
  • 5.1. Analyzable Programs (D.2)
  • 5.2. Boundary Value Analysis (D.4)
  • 5.3. Control Flow Analysis (D.8)
  • 5.4. Data Flow Analysis (D.10)
  • 5.5. Defensive Programming (D.14)
    • 5.5.1. Data should be range checked
    • 5.5.2. Data should be dimension-checked
    • 5.5.3. Read-only and read-write parameters should be separated and their access checked
  • 5.6. Functions should treat all parameters as read-only
    • 5.6.1. Literals and constants should not be write-accessible
    • 5.6.2. Using GNAT SAS and SPARK to drive defensive programming
  • 5.7. Coding Standards and Style Guide (D.15)
  • 5.8. Equivalence Classes and Input Partition Testing (D.18)
  • 5.9. Error Guessing (D.20)
  • 5.10. Failure Assertion Programming (D.24)
  • 5.11. Formal Methods (D.28)
  • 5.12. Impact Analysis (D.32)
  • 5.13. Information Encapsulation (D.33)
  • 5.14. Interface Testing (D.34)
  • 5.15. Language Subset (D.35)
  • 5.16. Metrics (D.37)
  • 5.17. Modular Approach (D.38)
    • 5.17.1. Connections between modules shall be limited and defined, coherence shall be strong
    • 5.17.2. Collections of subprograms shall be built providing several level of modules
    • 5.17.3. Subprograms shall have a single entry and single exit only
    • 5.17.4. Modules shall communicate with other modules via their interface
    • 5.17.5. Module interfaces shall be fully documented
    • 5.17.6. Interfaces shall contain the minimum number of parameters necessary
    • 5.17.7. A suitable restriction of parameter number shall be specified, typically 5
    • 5.17.8. Unit Proof and Unit Test
  • 5.18. Strongly Typed Programming Languages (D.49)
  • 5.19. Structure Based Testing (D.50)
  • 5.20. Structured Programming (D.53)
  • 5.21. Suitable Programming Languages (D.54)
  • 5.22. Object Oriented Programming (D.57)
  • 5.23. Procedural Programming (D.60)
• 6. Technology Annex
  • 6.1. Ada Programming Language
    • 6.1.1. Qualification
    • 6.1.2. Annex D References
  • 6.2. GNAT Pro Assurance Toolsuite
    • 6.2.1. Qualification
    • 6.2.2. Run-Time Certification
    • 6.2.3. Annex D References
  • 6.3. SPARK Language and Toolsuite
    • 6.3.1. Qualification
    • 6.3.2. Annex D References
  • 6.4. GNAT Static Analysis Suite
    • 6.4.1. Defects and Vulnerability Analysis
      • 6.4.1.1. Qualification
      • 6.4.1.2. Annex D References
    • 6.4.2. Basic Static Analysis tools
      • 6.4.2.1. Qualification
      • 6.4.2.2. Annex D References
  • 6.5. GNAT Dynamic Analysis Suite
    • 6.5.1. Qualification
    • 6.5.2. Annex D References