Scheda programma d'esame
SOFTWARE VALIDATION AND VERIFICATION
FABIO GADDUCCI
Anno accademico2018/19
CdSINFORMATICA
Codice660AA
CFU9
PeriodoPrimo semestre
LinguaInglese

ModuliSettoreTipoOreDocente/i
SOFTWARE VALIDATION AND VERIFICATIONINF/01LEZIONI72
FABIO GADDUCCI unimap
Obiettivi di apprendimento
Learning outcomes
Conoscenze

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.

Knowledge

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.

Modalità di verifica delle conoscenze

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.

Assessment criteria of knowledge

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.

Capacità

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.

Skills

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.

Modalità di verifica delle capacità

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à.

Assessment criteria of skills

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.

Comportamenti

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à.

Behaviors

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.

Modalità di verifica dei comportamenti

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.

Assessment criteria of behaviors

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.

Prerequisiti (conoscenze iniziali)

Conoscenze di base di logica proposizionale e di teoria degli automi.

Prerequisites

Some basic knowledge of propositional logics and automata theory.

Corequisiti

Nessuno.

Co-requisites

None.

Prerequisiti per studi successivi

Nessuno.

Prerequisites for further study

None.

Indicazioni metodologiche

Il corso si basa su lezioni frontali e sessioni di esercizi.

Teaching methods

The course is based on lectures and exercise sessions.

Programma (contenuti dell'insegnamento)

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*
Syllabus

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
Bibliografia e materiale didattico

Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.

Bibliography

Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.

Indicazioni per non frequentanti

Slide e testi di esercizi sono resi disponibili sul sito del corso.

Non-attending students info

Slides and exercise sheets are available on the course web page.

Modalità d'esame

Verifica intermedia (in alternativa, una prova orale) e un seminario su uno degli argomenti avanzati discussi durante il corso.

Assessment methods

Mid-term (alternatively, an oral examination) plus a talk on one of the advances topics discussed during the course.

Altri riferimenti web

Nessuno.

Additional web pages

None.

Note

Nessuna.

Notes

None.

Ultimo aggiornamento 29/10/2018 21:50