CdSINFORMATICA
Codice660AA
CFU9
PeriodoPrimo semestre
LinguaInglese
| Moduli | Settore/i | Tipo | Ore | Docente/i | |
| SOFTWARE VALIDATION AND VERIFICATION | INF/01 | LEZIONI | 72 |
|
Lo scopo del corso è quello di introdurre tecniche per la verifica e la validazione delle proprietà del software, sia estraendo un modello da un programma e verificandolo, sia testando il software prima della successiva distribuzione, sia dotando il software di strumenti in grado di monitorare la sua esecuzione.
The aim of the course is to introduce techniques for the verification and validation of software properties, either by extracting a model from a program and verifying it, either by testing the software before the next distribution, or by equipping the software with tools for monitoring its execution.
L'esame consiste in una prova scritta (ed eventualmente una orale) e un seminario su un argomento avanzato solo accennato durante il corso. La prova scritta e l'eventuale prova orale hanno l'obiettivo di accertare che lo studente abbia acquisito sufficiente familiarità con i concetti di base legati alla logica temporale lineare e alla sua verifica. Il seminario quello di verificare la capacità dello studente nell'affrontare temi allo stato dell'arte riguardo l'uso di metodi formali per la specifica e la verifica del software.
The exam consists of a written test (and possibly an oral one) and a seminar on an advanced topic only mentioned during the course. The written test and the possible oral test have the objective of ascertaining that the student has acquired sufficient familiarity with the basic concepts related to linear time logic and its verification. The seminar is to verify the student's ability to address state-of-the-art topics regarding the use of formal methods for specifying and verifying software.
Al termine del corso lo studente sarà in grado di utilizzare tecniche formali e tool allo stato dell'arte per quel che riguarda la specifica e la verifica software, con particolare attenzione per il model checking.
At the end of the course the student will be able to use formal techniques and state-of-the-art tools with regard to software specification and verification, with a particular focus on model checking.
Alcune lezioni sono completamente dedicate alla soluzione guidata di esercizi al fine di far meglio comprendere sia le potenzialità espressive (rispetto alle proprietà del software) dei linguaggi di specifica introdotti nel corso che le difficoltà che si incontrano nello sviluppare tool per la verifica automatica di tali proprietà.
Some lessons are completely dedicated to developing the solution of exercises in order to better understand both the expressive potential (with respect to software properties) of the specification languages introduced in the course and the difficulties encountered in developing tools for the automatic verification of these properties.
Al termine del corso lo studente avrà acquisito maggiore consapevolezza sull'importanza di descrivere formalmente le proprietà desiderate del software e posto in contesto alcune delle tecniche attualmente utilizzate per quel che riguarda sia la specifica che la verifica di dette proprietà.
At the end of the course the student will have acquired the awareness of the importance of formally describing the desired properties of the software and put into context some of the techniques currently used for what concerns both the specification and the verification of said properties.
Le esercitazioni permettono di verificare la sensibilità del gruppo rispetto all'importanza nella pratica dei temi trattati durante il corso, mentre la prova seminariale consente di evidenziare la capacità del singolo nell'inquadramento generale dello specifico argomento trattato.
The exercises allow to verify the awareness of the group with respect to the importance in practice of the topics covered during the course, while the seminar allows to highlight the ability of the individual in the general framework of the subject matter of the seminar.
Conoscenze di base di logica proposizionale e di teoria degli automi.
Some basic knowledge of propositional logics and automata theory.
Nessuno.
None.
Nessuno.
None.
Il corso si basa su lezioni frontali e sessioni di esercizi.
The course is based on lectures and exercise sessions.
Specifica delle proprietà del software
- Asserzioni
- Proprietà degli invarianti, safety e liveness, fairness
Model Cheking Proprietà di Linear Time
- Sistemi di transizione e grafici del programma
- Controllo delle proprietà di safety regolari
- Controllo delle proprietà omega-regolari con gli automi di Büchi
Logiche Linear Time
- Forme normali positive
- Fairness
- Model checking formule LTL
Logiche Computational Tree
- Model checking formule CTL e CTL*
Specifying software properties
- Assertions
- Invariants, Safety and Liveness Properties, Fairness
Model Cheking Linear Time Properties
- Transition systems and Program graphs
- Checking regular safety properties
- Checking omega regular properties with Büchi automata
Linear Time Logics
- Positive Normal Forms
- Fairness
- Model checking LTL formulas
Computational Tree Logics
- Model checking CTL and CTL* formulas
Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.
Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.
Slide e testi di esercizi sono resi disponibili sul sito del corso.
Slides and exercise sheets are available on the course web page.
Verifica intermedia (in alternativa, una prova orale) e un seminario su uno degli argomenti avanzati discussi durante il corso.
Mid-term (alternatively, an oral examination) plus a talk on one of the advances topics discussed during the course.
Nessuno.
None.
Nessuna.
None.