tutorial-ABZ-2023

Using B to program the CLEARSY Safety Platform Starter Kit For Education
This tutorial presents the programming model, based on B, of the CLEARSY Safety Platform, through a number of examples. These examples are exploited to demonstrate how the platform could be used for education, bridging the gap between formal methods and embedded systems / automation.
Update: slides (introduction, programming model, exercices list) are now available.

Organisers
The tutorial is given by:

• Dalay ALMEIDA (Safety Engineer), involved in the research and the education over the CLEARSY Safety Platform.
• Florain JAMAIN (Safety Engineer), involved in the education over the CLEARSY Safety Platform.
• Thierry LECOMTE (R&D Director), involved in the development of the CLEARSY Safety Platform for Education.

This tutorial is heavily based on the courses and seminars given in different engineering schools and universities in Brasil, Canada, France, Italy, Japan, Norway, Portugal, and UK.

Attending
The tutorial will be run within the framework of the ABZ 2023 international conference (https://abz2023.loria.fr/). It will take place on Tuesday May 30th, from 15:45 to 18:45 in the amphithéatre A008 Jean Legras.

Participating
3 possibilities are offered:

• listening to the tutorial
• listening and doing the exercices with the software simulator (Windows only, self-sufficient 550 Mo archive)
• listening and doing the exercices with the SK0 board connected through a USB host port (Windows only, self-sufficient 550 Mo archive)

Outline (Duration : 3 hours)

1. Introduction
   1. Overview, key features, applications
   2. Installing and setting up the environment
2. Programming model
   1. Design principles "à la ARDUINO"
   2. CLEARSY Safety Platform project specifics
   3. Process: modelling, verification, code generation
3. Exercices
   1. Simple: Not, or / 3-bit adder / clocks / flasher / deadman / filter / secret code / SOS
   2. More complex: traffic lights management
4. Conclusion

Resources
Directions, slides, models, and source code are hosted at https://github.com/CLEARSY/tutorial-ABZ-2023.
Software (Atelier B 24.04 CLEARSY Safety Platform) is available at https://www.atelierb.eu/en/atelier-b-support-maintenance/download-atelier-b/.
Slides (intro, programming model, exercice list) have been released.
Models (solutions to exercices) will be released after the tutorial.

Requirements
To follow the tutorial, participants are expected to bring their laptops and to have Windows 10 or 11 installed (natively or through a VM). A number of skills/knowledge is also expected from participants:

• intermediate software development,
• comfortable with formal logic,
• knowledge/experience with B or Event-B.

Skills learned

• introduction to safety computer
• programming a logic controller with B

Contributers
Nicolas Ayache, François Guignot, Florian Jamain, Thierry Lecomte

Shield:

This work is licensed under a Creative Commons Attribution 4.0 International License.