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.
Organisers The tutorial is given by:
- 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/).
Outline (Duration : 3 hours)
- Introduction
- Key concepts
- Development cycle
- The CLEARSY Safety Platform (CSSP) for education
- The programming model
- Modelling with B for CSSP
- Exercices: 3-bit adder, clock, deadman checker, filter, traffic lights, valve, track circuit, pumps, airlock
- Conclusion
Resources
Directions, software (IDE), slides, models, and source code are hosted at https://github.com/CLEARSY/tutorial-ABZ-2023
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
