R&D Activities
– B Projects
CLEARSY conducts R&D projects in various contexts: subsidized projects (Europe, France or regional) and internal projects. The table below shows the latest public research projects in which CLEARSY has been actively involved.
THEMES
THESE RESEARCH PROJECTS MAKE IT POSSIBLE TO TACKLE NEW THEMES AND EXPLORE INNOVATIVE TOPICS SUCH AS
AUTOMATION AND CONFIDENCE LEVEL OF THE AUTOMATIC PROOF PROCESS
The mathematical proof of B-models avoids unit testing and much of the integration testing of the resulting software. This mathematical proof is a not fully automated process (human intervention is required to complete some demonstrations) that relies on a single tool (validated with other proof tools as well as human expertise). Connecting to other proof tools increases both the rate of automatic proof (reducing human intervention) and the level of confidence in the results (when two tools, developed with different technologies and by separate teams, arrive concomitantly at the same positive conclusion).
THE EXTENSION OF FORMAL VALIDATION OF CONSTANT DATA
Formal validation of constant data is applied today by almost all the players in the railway world, particularly for the validation of track data. It allows the verification that the parameterisation of a system, in the broadest sense of the term, is acceptable with respect to rules defining this acceptability. The rules are formalised using the mathematical language of B and the acceptability check is carried out by the ProB model-checker. For decision security purposes, a second verification tool, PredicateB++, is used to confirm a positive decision by ProB. This approach is currently being intensively deployed with many industrial companies in the railway sector. The property modelling language is extended while the input and output interfaces are diversified.