Who watches the watchers: Validating the ProB Validation Tool
This work is incremental, focusing on validating an existing tool for safety-critical railway applications to meet stringent integrity requirements.
The paper addresses the need for rigorous validation of the ProB tool, which has evolved from a complementary proving tool to a primary development environment for safety-critical applications like exhaustive model checking and data validation in the railway domain, and it summarizes validation efforts conducted within the context of the EN 50128 norm.
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.