Who watches the watchers: Validating the ProB Validation Tool

TL;DR

This paper details the validation process of ProB, a tool increasingly used for critical applications like model checking and data validation, emphasizing compliance with safety standards in the railway industry.

Contribution

It presents a comprehensive validation approach for ProB, aligning it with safety standards such as EN 50128 for railway safety-critical systems.

Findings

ProB meets safety validation standards for railway applications.

Validation enhances trust in ProB for critical safety tasks.

The process ensures ProB's reliability in safety-critical contexts.

Abstract

Over the years, ProB has moved from a tool that complemented proving, to a development environment that is now sometimes used instead of proving for applications, such as exhaustive model checking or data validation. This has led to much more stringent requirements on the integrity of ProB. In this paper we present a summary of our validation efforts for ProB, in particular within the context of the norm EN 50128 and safety critical applications in the railway domain.