Versione definitiva
Introduzione ai metodi formali nel software e nei servizi. Uso di logiche per esprimere specifiche e proprietà statiche e dinamiche: logica del prim'ordine, query al prim'ordine, query congiuntive. logiche descrittive, logiche temporali e logiche dinamiche.
Metodi formali: analisi e verifica di aspetti statici.
Sintassi e semantica formale dei diagrammi concettuali, quali diagrammi delle classi UML e diagrammi Entità Relazione, verifica di proprietà statiche, uso di logica del prim'ordine e di logiche descrittive per il ragionamento automatico su tali diagrammi. Interrogazioni su diagrammi UML. Uso delle logiche descrittive, ALC, ALCQI, DL-LiteA. Ragionamento su logiche descrittive: procedure basate su tableaux per ALC. Query answering di query congiuntive (e unioni di query congiuntive) in logiche descrittive: procedure basate su perfect-rewriting in DL-LiteA. Query epistemiche*.
Metodi formali: analisi e verifica di aspetti dinamici.
Semantica operazionale astratta dei programmi: semantica di valutazione (intera computazione) e semantica di transizione (singolo passo della computazione). OCL cenni. Precondizioni, postcondizioni e invarianti di un programma. Correttezza parziale e totale. Programmi reattivi/interattivi (a stati finiti) reattivi come sistemi di transizione (cf. semantica di transizione), astrazione. Verifica di proprietà dinamiche e temporali su sistemi di transizione: Safeness, Liveness, Fairness, Strong Fairness. Logiche temporali per la verifica: LTL e CTL. Model checking per CTL. Il sistema SMV. Model checking simbolico: OBDD*. Model checking per LTL.
Gli argomenti contrassegnati con * non sono nel programma di coloro che devono sostenere l'esame nella modalità 5 CFU (eg. Metodi formali nell'ingegneria del software - ordinamento 2000).