Using B to program the CLEARSY Safety Platform

Tuesday, 08.06.21, 14:00 - 16:00

Table of Contents

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 ( 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.


With this tutorial, you are going to learn on a concrete example how to use a formal method for "serious thing" - that is far more than model, predicate and proof. We will have a look at:

A level crossing controller is going to be exercised with several boards and different environments to demonstrate how the CLEARSY Safety Platform could be used for safety critical applications, see image on github.


Tuesday, 08.06.21, 15:30 - 17:30 (GMT+2), duration 2 hours

  1. Introduction
    1. Safety, standards & embedded systems
    2. The railway crossing example
    3. The CLEARSY Safety Platform in a nutshell
  2. The CLEARSY Safety Platform for education
    1. The starter kit SK0
    2. The software simulator (VM)
    3. Implementing the level crossing controller
  3. The CLEARSY Safety Platform for industry
    1. The safety core computer CS0
    2. Implementing the level crossing controller
  4. Conclusion


Slides, models, and source code hosted are hosted at


Skills learned