First Practical Excersice of the course Formal Methods in Software Design at TU Darmstadt, which demonstrate the concept of Model Checking using Promela, and SPIN
Simulate a man in the middle Attack and the solution to prevent it using a parity bit to check for a change. Using the LTL Formel together with SPIN to check the correctness of the implementation
Simulate the N-Smoker problem and implement a simple solution to the problem (ordered actions) to solve possible deadlock. Using LTL Formel and never block to prove the correctness of the implementation of the solution.