Background and motivation

In the realm of railway software development, adhering to industrial standards is not just a matter of compliance; it’s a cornerstone of ensuring safe, reliable, and efficient railway systems. The latest milestone along this journey is the introduction of the CENELEC standard EN 50716:2023. This new standard represents a significant leap forward compared to its predecessors, EN 50128:2011 (and its amendments A1 and A2) and EN 50657:2017 while maintaining a smooth transition from its predecessors and a closer alignment with the railway RAMS standards (EN 50126 and EN 50129).
This development holds significant importance for us at Prover, given our intimate connections with these standards, wherein we provide EN 50128-compliant software tools and applications. Thus, we have thoroughly studied EN 50716 and are excited to share our findings and thoughts here in this blog post. Join us as we delve into the nuances of this latest standard, exploring both its implications and potential impacts.

Formal methods become HR for all SILs

The “Highly Recommended (HR)” endorsement of the Formal Methods technique has now extended to also include lower SILs (e.g., SIL 1 and SIL2 which used to be only R).

As a longstanding believer and practitioner of Formal Methods, we are delighted to see the further endorsement of EN 50716 for the technology. Thanks to advancements in technology and much-improved usability over the years, which Prover has contributed to, Formal Methods have become the efficient and cost-effective approach for rail systems they are today.

Tool diversity

Originating from Clause 6.7.4.4 c of EN 50128, the “tool diversity” concept was introduced in Amendment A2:2020 of EN 50128 and then included in EN 50716. The concept of tool diversity concerns classes T2 and T3 of tools. Model checkers (such as Prover PSL) and testing-related software utilities fall into the class of T2 tools, which is specifically designed for verifying code or data. In contrast, T3 tools are involved in the creation or transformation of code, commonly represented by code compilers and generators. Essentially, tool diversity allows T3 tools to delegate (some) trust to T2 tools, see a quote from the clause:

“Use one tool to perform the function and subject its output to verification of results by an independent tool… for example a rule-checking tool to confirm that the output conforms to all relevant rules.”

This represents a significant evolution from our perspective, as it aligns seamlessly with the principles of our Signaling Design Automation (SDA) solution Prover Trident, which was established many years ago. The independent T2 and T3 tools of the Prover Trident tool suite are Prover Certifier and Prover iLock, respectively. The application software code generated from Prover iLock (based on some GA) can be checked independently by Prover Certifier for conformance to formalized safety requirements (ref. “conforms to all relevant rules”). Therefore, the evidence for Prover iLock working correctly and safely can be based on the use of Prover Certifier, which is highly trusted and certified by TÜV NORD as a CENELEC EN50128-compliant T2 tool for SIL 4 applications.

Annex C

This annex in EN 50128 has been replaced with Annex C “Guidance on software development” in the new standard EN 50716, which now consists of the following three very interesting sections:

• “C.1 Lifecycle model examples”,
• “C.2 Modelling”, and
• “C.3 Artificial Intelligence and Machine Learning”.

Lifecycle models

Section C.1 provides guidance and examples regarding two lifecycle models, i.e., linear lifecycle models (such as the waterfall and v model) and iterative lifecycle models. Linear lifecycle models offer a structured and predictable approach to software development, widely considered the conventional choice. The iterative lifecycle models, on the other hand, prioritize flexibility and responsiveness (to changes), albeit requiring more frequent communication and coordination among team members.

There has been a growing interest in applying iterative models (or agile methodologies) in safety-critical systems including rail systems. We find it interesting that iterative lifecycle models are explicitly accepted by the standard. However, adopting these iterative lifecycle models requires careful consideration to balance flexibility and safety assurance, ensuring that safety and regulatory requirements are adequately addressed. Achieving such a balance can be facilitated by leveraging a model-based approach, adaptability (e.g., utilizing tool diversity as described above), and rigorous methods such as Formal Verification. The automation embedded in formal verification processes enables the assurance of safety with reduced verification times and great certainty. Prover’s SDA approach fits this profile perfectly.

Modeling

In Section C.2, the advantages of modeling approaches are explored, and guidance is provided regarding their application in the context of the standard.

At Prover, we are also excited by this new inclusion in the standard, as modeling (using our formal languages such as PiSPEC, LCF and HLL) serves as one of the cornerstone techniques in the Prover Trident solution and the Digital Twin approach. As highlighted in the excerpt from the standard below, the modeling approach brings even greater benefits when combined with Formal Verification (using formal proofs):

“Models can also reduce the need for certain activities, particularly when using formal proofs.”

AI/ML

Artificial Intelligence (AI), in particular Machine Learning (ML) as the most relevant among the AI areas, is discussed in Section C.3, with respect to the difficult challenges to be addressed in the context of applications in the scope of EN 50716. Because of the challenges (e.g., the V&V of ML components), the ML techniques have not yet become viable techniques for rigorous software development within the standard.

While we agree that it is natural to have such concerns about ML given its inherent characteristics (such as statistical modeling and interpretability), from a different perspective, we at Prover have started to explore how ML techniques can accelerate the adoption of Formal Methods. For more details, see our blog post on AI.

Improvements in management and organization

Following a significant refinement for Clause 5, the requirements on software management and organization have become more concise, succinct, and in some cases relaxed, thereby facilitating users to navigate standards with greater ease and flexibility.

One example of removing/relaxing unrealistic restrictions is the fact that changing the roles of Verifier and Validator is no longer prohibited (but is still discouraged) as outlined in Subclause 5.1.2.10 f of EN 50716, compared to Clause 5.1.2.4 of EN 50128.

The role of Integrator in EN 50128 is removed from EN 50716 and the responsibilities of the role fall under the roles of Implementer and Tester. Instead of the Integrator, the Implementer is supposed to manage the integration process, whereas the Tester is supposed to take responsibility for writing relevant specifications such as the Software Integration Test Specifications and the Software/Hardware Integration Test Specification.

The “Safety Authority” body is no longer relevant in EN 50716. For example, the Assessor has the flexibility to belong to any stakeholder organization without requiring the approval of the “Safety Authority”, as outlined in Subclause 5.1.2.5.

Miscellaneous changes

There are also some changes of various kinds we find interesting and worth highlighting here.

1. EN 50716 switched to “Basic Integrity” defined in EN 50126 and stopped using “SIL 0”, which probably corresponds to one change described in the foreword: “Better alignment with EN 50126-1:2017 and EN 50126-2:2017, including definitions, has been made;”
2. Some justifications and documents are no longer required for the T2 tools used for Basic Integrity. See e.g., Subclauses 6.7.4.2 and 6.7.4.3.
3. Programming languages can also refer to diagrammatical or modeling languages rather than just textual programming languages (such as C, C++, Java, etc.). Additionally, Clause 7.3 (Architecture and Design) introduces criteria for choosing suitable programming languages, which in part replace the requirements related to the fitness for purpose of programming languages (Subclause 6.7.4.7 of EN 50128).
4. In EN 50716, the term “application algorithms” has been removed from the title of Clause 8. This change may clarify that this clause primarily addresses the requirements for application data rather than generic or application software. The application data primarily consists of parameterization information for specific installations and the application software defines the intended behavior (or logic) of specific applications. Prover iLock is a complete development process for signaling systems, particularly application data and software. Hence it is part of our continuous endeavor to maintain its compliance with Clause 8 of EN 50716.

Conclusion

In summary, here at Prover we are leading the way when it comes to embracing the latest advancements within the standard, while continually enhancing our solutions and products to closely align with the requirements of EN 50716. Our dedication ensures that our customers and partners are fully equipped to meet these requirements and thrive in their endeavors.