Using B to program the CLEARSY Safety Platform

This tutorial presents the programming model of the CLEARSY Safety Platform to specify, develop and prove command and control applications with B. A number of examples are exploited to demonstrate how the platform could be used for education, bridging the gap between formal methods and embedded systems / automation.

The tutorial is given by Thierry LECOMTE. Thierry LECOMTE is R&D Director at CLEARSY and has been involved in safety and security formal modelling research for decades. He led the LCHIP (Low Cost High Integrity Platform) project during 4 years to build up the CLEARSY Safety Platform.

This tutorial completes the talk "Programming the CLEARSY Safety Platform" by providing more practical details on how to use it for education and research. This tutorial was first given during the RSSR 2017 conference (https://conferences.ncl.ac.uk/rssrail/tutorials/#tut2). The tutorial proposed for ABZ 2021 will contain more material based on feedback collected from teachers. It will also present the evolution from the SK0 board, its simulation-based software only version released in 2021 and its industry version, coming with a more open programming model.

Outline

TBA.