ABSTRACT. During this tutorial I will introduce the main features of {log} from the user perspective. More specifically, I will show: • How the main elements of B and Z specifications can be encoded in {log}. • How the resulting {log} forgram can be executed in order to run different scenarios as a first analysis of the model. • How to write and generate verification conditions and how they can be automatically discharged in {log}. • Some (theoretical) tips on determining when a verification condition fits inside of one of the decision procedures implemented in {log}.

ABSTRACT. Due to the simplicity and flexibility of the language and intuitive and automatic feedback provided by its analyzer, Alloy (http://alloytools.org) is often taught in introductory formal methods courses (https://alloytools.org/citations/courses.html). However, the classic standalone Alloy Analyzer suffers from some limitations that hinder its usage in the classroom, namely i) the lack of a straightforward mechanism to share simple Alloy models, instances and associated themes, a process that becomes cumbersome in large classes where students require feedback or have to submit exercise resolutions for evaluation; and ii) the absence of some automated assessment functionality or online judge system for students to autonomously solve exercises and receive automatic feedback regarding the correctness of their resolutions. The Alloy4Fun platform (http://alloy4fun.inesctec.pt/) was developed precisely to address these issues. Alloy4Fun allows users to edit and execute Alloy 6 models online, providing a minimalistic customizable instance visualizer. Both models and instances can be easily shared through permalinks. Moreover, the platform provides support for simple specification challenges in the form of duels where students attempt to discover a secret constraint specified by the instructors. When solving these challenges, students are supported by a hint system to nudge them in the right direction when stuck. Alloy4Fun collects anonymized information about the student submissions and interactions, so that instructors can measure the progress of the students on the shared challenges and identify potential learning bottlenecks.

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

You can get access at https://github.com/CLEARSY/tutorial-ABZ-2023 ?