AdaCore provides rail software developers with the advanced tools and development environment they need to streamline their process and meet the demands of creating certified rail applications.
The highest priority in the railway industry is safety. As a result, a significant amount of time and energy is invested in code-review and testing activities. With rail developments now involving more and more electronics, including railway control software, there is an even heavier draw on software development resources.
There is also a move towards lower costs and shorter project timescales. While developers are looking at COTS technologies to bring lower costs and speedier development, there remain key challenges to managing the complexity of a rail system, providing long-term support, and maintaining the conformance of the system to evolving safety and security standards. In order to meet the demand, without compromising safety or quality, industry has recognized the need for tools that allow it to work more efficiently.
AdaCore has years of experience working with customers in the rail industry and understands the complexities of developing rail applications. We help developers address those challenges with tools and services that help the workflow, ensure reliability and manage costs.
Certification for Rail - CENELEC EN 50128
AdaCore has extensive experience helping rail customers meet the CENELEC EN 50128 certification requirements. Today, railway projects are subject to qualification standards that define certain objectives in terms of reliability, availability, maintainability and safety. The standards governing safety systems have been quickly evolving over time to achieve better certifiability of systems and more effective product lifecycle management. CENELEC EN 50128 is the European standard used to certify rail applications. It classifies criticality levels between SIL0 (lowest) to SIL4 (highest). This is the most demanding international standard for safety integrity concerning software for railway control and protection. AdaCore's solution for CENELEC EN 50128 is a certifiable and qualifiable software development toolset based on the Ada and SPARK languages.
Read our booklet on CENELEC EN 50128:2011
Jean-Louis Boulanger & Quentin Ochem
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
AdaCore’s technology can be used at all levels, from SIL 0 to SIL 4
Using Ada and SPARK allows to reduce overall verification and certification costs. This is achieved through a language designed to minimize the introduction of programming errors and to support expression of interface and component specification directly in the source code. This enables fewer defect rate and early verification and error detection, minimizing the amount of issues caught later in the process when fixes require more resources.
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 GNAT 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."
Qualified Tools, Runtime Libraries and Certification Materials
Several of our tools have been qualified, thus reducing the effort to meet verification objectives including coding standard compliance, code accuracy (prevention of errors such as buffer overrun, integer overflow, and references to uninitialized variables), and structural coverage analysis up to MC/DC. Specialized high-assurance run-time libraries, including one that implements the Ravenscar tasking profile, are simple enough to be included in certified systems but expressive enough to support the needed functionality for hard real-time avionics software. Qualification and certification material for these tools and libraries is available and is adaptable to new project contexts.
Sustained Branches
Maintaining certified software brings unique challenges, since the customer needs to "freeze" on a specific version of the technology for stability, but still might require updated releases if a problem is encountered as the software evolves. AdaCore has a special subscription service, known as a "sustained branch", that supports this requirement.
Customer Projects: Rail
Siemens
Siemens Switzerland Selects AdaCore Toolset for Railway Project
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.
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.
SPARK Pro
SPARK Pro is a language and toolset specifically designed for developing applications where correct operation is vital for safety or security. The SPARK Pro toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset generates evidence for correctness that can be used to meet the requirements of safety and security certification schemes.
GNAT Static Analysis Suite
GNAT SAS helps developers gain a deep understanding of their code and build more reliable and secure software systems. GNAT SAS features an Ada source code analyzer that detects run-time and logic errors. It assesses potential bugs and vulnerabilities before program execution, serving as an automated peer reviewer, helping to find errors easily at any stage of the development life-cycle. It helps you improve the quality of your code and makes it easier for you to perform safety and/or security analysis.
GNATcoverage
GNATcoverage allows coverage analysis of both object code (instruction and branch coverage), and Ada or C language source code (Statement, Decision and Modified Condition/Decision Coverage - MC/DC)