4th International ABZ 2014 Conference

ASM, Alloy, B, TLA, VDM, Z
June 2 - 6 2014
Toulouse - France


Formal Data Validation

One day Tutorial. June 3rd 2014.
Toulouse - France


Thierry LECOMTE (ClearSy, France). R & D Director
Michael LEUSCHEL (Düsseldorf University, Germany) - Professor of Computer Science

Information available on http://www.data-validation.fr/

During Rodin and DEPLOY EU-funded projects, track topology data model were developed in order to check real word railway system architectures. This data model is of paramount importance, as it is a strong precondition for software to behave safely (for example, if a signal is badly positioned, a collision is likely to occur). Validation of concrete data is complex because of the large amount of data (50k-100k excel cells, modified several times during a development) and the number of verifications to perform (up to 1000 rules, expressing intricate graph-based properties) over this dataset. As a consequence, human-based verification is time-consuming and subject to many mistakes. Automating the process, by formalizing the data model with the mathematical language of the B method and by performing the verification with the model-checker and constraint solver (ProB) has lead to dramatically reduced verification time from months to minutes.

During this tutorial, formal data validation principles will be exposed (key concepts, mathematical language to express properties, tool chain) and applied to simple examples covering different aspects.