Formal implementation of data validation for railway safety-related systems with OVADO

Abstract

This paper describes the process of data validation for railway safety-critical computer-based systems formally implemented by Systerel as supplier of railway industry's companies. More precisely, it describes the validation of data against the requirements it has to meet to ensure systems safety. International standards, especially CENELEC EN 50128, recommend the use of formal methods for designing the most critical safety-related systems. We use the OVADO formal tool to perform data validation. For that, we model data requirements by using the specification language of the B method, namely the B language, before using OVADO that automatically checks that data meet requirements. This tool integrates two independent components that must give the same results when they are applied on the same data, according to the principle of redundancy. An example of data validation for a CBTC system is also given. © 2014 Springer International Publishing.