Specifica e verifica di sistemi critici

The course aims to present methodologies and techniques for the rigorous specification and formal analysis of critical software systems, i.e., systems whose malfunction and vulnerabilities can cause unacceptable damage. It then presents theoretical foundations and tools for the formal specification based on Abstract State Machines, and the formal verification of properties expressed in temporal logic.

At the end of the course, the student will be able to develop the formal specification of a critical system and validate the specification. The student will also acquire the ability to specify complex requirements through model refinement, and how to guarantee the correctness, safety, and security of the system through model checking of properties in temporal logic.