Final project for the MSc course Formal Methods for Concurrent and Real-Time Systems a.y. 23/24 at Politecnico di Milano.
UPPAAL model for search and rescue of civilians during an emergency, carried out by trained professional assisted by autonomous drones.
This document presents the developed models (both non-stochastic and stochastic), the design choices behind them, meaningful properties and their formal verifications, with the final objective of highlighting strengths and weaknesses.