The goal of the project is to explore the validation and verification of a realistic safety-critical software system during the design and implementation stages of development.

It has two main parts:

1. Model and analyse the design of a critical system using Alloy;
2. Implement and verify a component of a safety-critical system using Dafny.

The problem is based on a real-life case study made by ABZ conference. Its specification can be found here.

This project was made by Alexandre Abreu and Breno Accioly for the Formal Methods for Critical Systems course at FEUP in 2021/2022.