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:
- Verification tool development, by RATP, initally based on PredicateB predicate calculus engine (part of Brama Event-B model animator), then completed by the ProB model-checker;
- data validation conducted by Siemens Transportation Systems, relying on the ProB model-checker, during the DEPLOY european project;
- data validation and generation conducted by Alstom Transportation Systems, relying on the ProB model-checker, and leading to the creation of a new kind of Atelier B project: data validation/generation.
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.