SSD

Crediti

INF/01

8

Obiettivi Formativi

L’obiettivo del corso è di presentare le metodologie e le tecniche per la specifica e l’analisi formale di sistemi complessi. Vengono quindi presentati i fondamenti teorici delle metodologie di modellazione astratta (operazionale e dichiarativa) e delle tecniche di verifica formale di proprietà espresse in logica temporale.

Competenze acquisite

Al termine del corso, lo studente dovrà essere in grado di sviluppare un modello di specifica formale per un sistema complesso. Lo studente inoltre dovrà aver acquisito una capacità di modellazione tramite raffinamento di modelli ed avere competenze su metodi e tecniche per la verifica formale di proprietà temporali.

Programma

– Introduzione: Cosa sono ed a cosa servono i Metodi Formali. Applicazione dei Metodi Formali alla progettazione ed all’analisi di sistemi.
– Modellazione ed analisi ad alto livello di astrazione: Le Abstract State Machines (ASM). Tecniche di raffinamento di modelli. Il tool-set ASMETA per modelli ASM. Casi di studio di specifica di sistemi.
– Modellazione ed analisi a basso livello di astrazione. Automi di Kripke e Logica Temporale CTL: sintassi, semantica, pattern di specifica. Algoritmi di model checking. Simbolic Model Checking con rappresentazione mediante OBDD. Verifica di proprietà temporali: proprietà di raggiungibilità, di safety, di liveness, di fairness, assenza di deadlock. Astrazione di modelli: fusione degli stati; astrazione di variabili, riduzione di variabili, observer automata. Raffinamenti di modelli: mappatura di modelli ad alto livello di astrazione verso modelli temporali.

Testi Consigliati

– Materiale fornito dal docente

Modalità di Verifica

–         Prova scritta con domande aperte e scelta multipla

–         La durata della prova e di massimo 2 ore

–         La valutazione viene espressa in trentesimi