Data Validation / Generation

Data validation and generation are of paramount importance in the railways, in order to ensure safety at the system level.

Several studies/works have been conducted the past years:

Data validation consists in ensuring that metro line exploitation data (such as track topology, equipement psotionning, etc.) comply with a given corpus of signalling rules. This data, uploaded on board safety critcal devices, directly contribute to the safety of the whle system and should be validated as such. This validation has been mainly manual because of the large set of data to manipulate (up to 100,000 data chunks and several hundreds rules).

Progress made in the domain of model-checking (and by ProB in particular) has enabled the building of data models, based on the B mathematical language, and their automated verification against large data sets, in few hours (compared to several months when performed by humans), with a slightly better level of confidence in the results obtained.

 

From a technical point of view, data models and data to validate are transformed in a B model that feeds ProB, with the objective of:

  • verifying that data are compatible with data model. ProB is able to provide all counter-examples, if any;
  • generate some data, if the data model is partly instanciated (some values are missing).

Data validation can be inserted in any development cycle, including the B development cycle.