The course aims at providing a systematic account of computer science methods, formalisms, and algorithms for the formal specification and automatic verification/validation of complex reactive systems. The student will learn how to master advanced formal tools (logic, automata theory, logical game theory) to be used for the analysis and the automatic verification of complex systems. See also this link.
Lesson 1: 03/03/2025 (10:30 - 12:30) 2 hours
Description: Introduction on the 2nd and 3rd module of the course: outline of the main topics that will be covered. Overview of automatic verification and validation technique, in particular to Model Checking. Introduction to the SMV modeling language: history and a first simple example.
Lesson 2: 04/03/2025 (10:30 - 12:30) 2 hours
Description: Syntax of SMV: the ASSIGN, init, and trans keywords. The CASE expressions. Semantics of SMV: transition system associated with an SMV module. Nondeterminism in SMV, implicit modeling, and input variables. Examples.
Lesson 3: 06/03/2025 (10:30 - 12:30) 2 hours
Description: SMV modules. Example of formal verification of a mechanical counter. Synchronous and asynchronous modeling: the PROCESS keyword. Fairness constraints: definitions of justice and compassion.