ECTS - University of Pisa
| Modules | Area | Type | Hours | Teacher(s) | |
| 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, or by testing the software before the 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 presentato 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 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 verifies 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 fully 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 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.
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
Model Cheking di Proprietà Linear Time
Logiche Linear Time
Logiche Computational Tree
Specifying software properties
Model Cheking Linear Time Properties
Linear Time Logics
Computational Tree Logics
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.
