At the occasion of the ABZ 2014 conference, a tutorial on formal data validation is organized at ENSEEIHT together with workshops (see details here). The tutorial will happen on June 3rd 2014 from 2:00 pm to 5:30 pm.
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.
The program is as follows:
- Introduction
- Formal Data Validation in a Nutshell
- Industrial Examples
- The approach: mathematical language et verification tools
- Case studies
If you want to attend the tutorial or get more information about this event, please contact thierry.lecomte@clearsy.com
Introduction
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.