Specification and Verification of Critical Systems
A.Y. 2025/2026
Learning objectives
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.
Expected learning outcomes
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.
Lesson period: Third four month period
Assessment methods: Esame
Assessment result: voto verbalizzato in trentesimi
Single course
This course cannot be attended as a single course. Please check our list of single courses to find the ones available for enrolment.
Course syllabus and organization
Single session
Responsible
Lesson period
Third four month period
Course syllabus
- Introduction: Safety and Security-critical systems. What are Formal Methods and what they are useful for. Using Formal Methods for systems design and analysis of critical systems.
- Modeling and analysis at high level of abstraction. The Abstract State Machines (ASM). Model refinement techniques. Model abstraction techniques. The ASMETA tool-set for ASM models. Case studies of system specification.
- Modeling and analysis at low level of abstraction. Kripke Automata and CTL temporal logic: syntax, semantics, specification patterns. Model checking algorithms. Symbolic Model Checking with OBDD. Temporal property verification: properties of reachability, safety, liveness, fairness, deadlock free. Model refinement: mapping high level abstraction models to low level abstraction temporal models. Tool: NuSMV model checker and AsmetaSMV.
- Modeling and analysis at high level of abstraction. The Abstract State Machines (ASM). Model refinement techniques. Model abstraction techniques. The ASMETA tool-set for ASM models. Case studies of system specification.
- Modeling and analysis at low level of abstraction. Kripke Automata and CTL temporal logic: syntax, semantics, specification patterns. Model checking algorithms. Symbolic Model Checking with OBDD. Temporal property verification: properties of reachability, safety, liveness, fairness, deadlock free. Model refinement: mapping high level abstraction models to low level abstraction temporal models. Tool: NuSMV model checker and AsmetaSMV.
Prerequisites for admission
Passing the exam in Logics is strongly recommended
Teaching methods
Lessons
Lab activities
Attending the teaching activities is strongly recommended
Lab activities
Attending the teaching activities is strongly recommended
Teaching Resources
1) Egon Boerger, Robert Staerk. Abstract State Machines. A Method for High-Level System Design and Analysis. Springer Verlag, 2003.
2) Michael Huth , Mark Ryan. Logic in Computer Science: modelling and reasoning about systems (2nd edition). Cambridge University Press, 2004.
3) B. Berard et al., System and Software Verification Model-Checking Techniques and Tools, Springer Verlag, 2001.
2) Michael Huth , Mark Ryan. Logic in Computer Science: modelling and reasoning about systems (2nd edition). Cambridge University Press, 2004.
3) B. Berard et al., System and Software Verification Model-Checking Techniques and Tools, Springer Verlag, 2001.
Assessment methods and Criteria
The exam consists of a written test and a practical test in the laboratory, both mandatory and both lasting two hours.
The written test focuses on checking the acquisition of skills on the theoretical aspects of the course; the practical test concerns the acquisition of the ability to use software environments for the specification, validation and verification of system properties.
Each test is evaluated in thirtieths, and the overall mark is the average of the marks reported in the two tests.
The written test focuses on checking the acquisition of skills on the theoretical aspects of the course; the practical test concerns the acquisition of the ability to use software environments for the specification, validation and verification of system properties.
Each test is evaluated in thirtieths, and the overall mark is the average of the marks reported in the two tests.
Professor(s)