PhD in Computer Science

Qualitative and probabilistic system verification

Qualitative and probabilistic system verification

Academic year 2015/2016

Sommario del corso

• Course objectives
• Learning assessment methods
• Program
• Teaching tools

Course objectives

make the students obtain experience of system verification techniques, which can be used in a number of different research areas. Furthermore, the course will introduce to the students the use of symbolic data structures such as decision diagrams; while these have been developed in the context of system verification, they can also be used in contexts in which an efficient representation of information is necessary.

Learning assessment methods

the exam has to be agreed on with the lecturer, but will principally comprise "hands-on" exercises with verification tools together with an theoretical analysis of a topic either not considered in depth during the course, or on a topic considered more exhaustively, in which case there will be a focus on the implications of the topic for the field of research of the student.

Program

1. Symbolic data structures and algorithms for their definition and manipulation: from the binary decision diagrams popularized by Bryant to multiterminal decision diagrams considered by Ciardo and other researchers, and their associated libraries. (Lecturer: Marco Beccuti)
2. Temporal logics (LTL and CTL) and their associated model-checking algorithms for the verification of concurrent programs (typically expressed by guarded command languages) and of models (networks of automata or Petri nets). Examples of properties that can be verified are: "for all executions, if a process requests an access of the critical region, then it will eventually have such access", "for all executions, for every message sent, the sender will eventually receive an acknowledgement" or "for every state along every possible execution, if the system enters in a malfunction state, then there exists an execution path from that state that reaches a state corresponding to correct operation". The logics LTL and CTL permit the formalization of such properties and to prove them automatically for programs with a potentially huge state space. (Lecturer: Susanna Donatelli)
3. The extension of temporal logics to the probabilistic/stochastic setting (the logics PCTL and CSL). Examples of properties of interest are: "with probability greater than 0.95 the system obtains a resource within K time units after requesting it", or "with probability greater than 0.9 the system converges to a stable state within N transitions, despite being in the presence of M users with fraudulent behaviour". (Lecturer: Jeremy Sproston)
4. Overview of other logics and verification techniques (this part will depend also on the areas of interest of the students).
5. Tools: for the verification of LTL and CTL we will use at least nuSMV (University of Trento, the free version of the well-known commercial tool SMV, based on binary decision diagrams) and the model checker of GreatSPN (developed by the University of Turin, based on multiterminal decision diagrams). For probabilistic and stochastic verification we will use PRISM (developed by the University of Birmingham and the University of Oxford) and possibly MC4CSLTA (developed by the University of Turin).

• Teaching materials
• Exams and finals
• Go to Moodle
• Visit the forums