Category Archives: Conference

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

Resources:

• slides

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.

ClearSy is contributing to a technical seminar organized by Newcastle University on 24 October 2013.

Formal methods are used worldwide to improve safety in several railways applications, at various levels and with a wide range of results obtained. This presentation is intended to provide a unified (not agnostic) overview of existing practices and to assess to which extent safety is ensured.

At that occasion, some examples of railways data validation will be exhibited.

ClearSy participated to CAI 2013 conference (International Conference on Algebraic Informatics) held in Porquerolles (France) 3-6 September 2013.

A talk, entitled “Railways formal data validation“, was given during the industrial session. It was a good occasion to expose to researchers the mathematical problems the railways industry is currently facing when validating safety-critical embedded data.