OTHER ACADEMIC YEARS

Automated Verification of Cyber-Physical Systems

Master Degree in Computer Science

University of L'Aquila

A.Y. 2023/2024

lecturer: Igor Melatti

igor.melatti@univaq.it

Index:

Exams

Course programme

Textbooks

Class material

Class timetable

Exams

Exams Rules

See lesson 1.

Available Papers

The following papers may be used for the paper-related exam:

Available Projects

Available projects are described in this document. As for the other resources mentioned in the document above, this is the paper describing the BUCK model and this is the file with the controllers to be used.

Exams Dates

N Date Hour Where Notes Deadline
1 13/06/2024 10:30AM - 11:30AM A1.3 Please discuss the project/paper with the lecturer in advance 09/06/2024 H23:59:59
2 27/06/2024 10:30AM - 11:30AM TBA Please discuss the project/paper with the lecturer in advance 23/06/2024 H23:59:59
3 11/07/2024 10:30AM - 11:30AM TBA Please discuss the project/paper with the lecturer in advance 07/07/2024 H23:59:59
4 05/09/2024 10:30AM - 11:30AM TBA Please discuss the project/paper with the lecturer in advance 01/09/2024 H23:59:59
straord
5 16/01/2025 11:00AM-01:00PM TBA Please discuss the project/paper with the lecturer in advance 12/01/2025 H23:59:59
6 30/01/2025 11:00AM-01:00PM TBA Please discuss the project/paper with the lecturer in advance 26/01/2025 H23:59:59
7 13/02/2025 11:00AM-01:00PM TBA Please discuss the project/paper with the lecturer in advance 09/02/2025 H23:59:59

Official information is here

Course Programme

Cyber-Physical Systems Modeling and Simulation

Statistical Model Checking

Probabilistic Model Checking

System Level Formal Verification

Textbooks:

Scientific papers provided by the lecturer

Class Material

N Date Material Arguments Notes
1 26/02/2024 slides Presentation of the course. Introduction to classical model checking techniques Slides 1-78
2 01/03/2024 see Lecture 1 Introduction to classical model checking techniques (contd)
3 04/03/2024 see Lecture 1 Introduction to classical model checking techniques (finished) Slides 79-end
4 08/03/2024 slides
comments		 Probabilistic Model Checking (part 1) Slides 1-46
5 11/03/2024 See slides and comments of lesson 4 Probabilistic Model Checking (part 2) Slides 47-64
6 15/03/2024 See slides and comments of lesson 4 Probabilistic Model Checking (part 3) Slides 65-87
7 18/03/2024 See slides and comments of lesson 4 Probabilistic Model Checking (part 4) Slides 88-128
8 22/03/2024 See slides and comments of lesson 4 Probabilistic Model Checking (part 5) Slides 129-174
9 25/03/2024 Review of the past lessons
10 05/04/2024 See slides and comments of lesson 4 Probabilistic Model Checking (part 6) Slides 175-195
11 08/04/2024 Review of the past lessons
12 12/04/2024 See slides and comments of lesson 4 Probabilistic Model Checking (part 7) Slides 196-245
13 15/04/2024 See slides and comments of lesson 4 Probabilistic Model Checking (part 8) Slides 246-360
14 19/04/2024 slides Simulation of CPSs (part 1) Slides 1-39
15 22/04/2024 Review of the past lessons
16 29/04/2024 Review of the past lessons
17 03/05/2024 Review of the past lessons
18 06/05/2024 See slides of lesson 14
modelica examples		 Simulation of CPSs (part 2) Slides 40-end
19 10/05/2024 slides Statistical Model Checking (part 1) Slides 1-23
20 13/05/2024 See slides of lesson 19 Statistical Model Checking (part 2) Slides 24-76
21 17/05/2024 See slides of lesson 19 Statistical Model Checking (part 3) Slides 77-102
22 20/05/2024 See slides in lesson 19
slides		 Statistical Model Checking (part 4). System Level Formal Verification (sketch) Slides 103-end and 1-101
23 24/05/2024 Review of students' projects/papers
24 27/05/2024 Review of students' projects/papers To be held in Digital class

Class Timetable

Day From To Where
Monday 9:30AM 11:30AM 0.6
Friday 9:30AM 11:30AM Digital Class

Room 0.6 is at the first floor of the "Renato Ricamo" building; it may be reached from the outside only.

The Digital Class is immediately outside the "Alan Turing" building, in a separate small house.