OVADO - Enhancing Data Validation for Safety-Critical Railway Systems

摘要

The safe behavior of railway software systems depends undeniably on the correctness of all data used by its components. Formal verification methods are nowadays successfully applied for the assessment of safety-critical systems in order to avoid inconsistencies, ambiguities or incompleteness. Unfortunately, these methods are rarely used by data validation tools, although they seem well-suited for this purpose. In this regard, RATP designed OVADO, a generic formal data-validation tool, which has been used in several projects covering a variety of data. This paper gives an overview of the past, present and future developments, applications and improvements of OVADO. It emphasizes how OVADO allowed RATP to be more efficient in its data validation process and how new enhancements will improve its usability, reliability and efficiency. OVADO's ease-of-use is, thereby, improved through the development of the B-OVADO editor. Additionally, the process is optimized with the definition of a common library for CBTC applications.