SITE TITLE

LOGO DIETI

Specifica di Sistemi

Titolo insegnamento in inglese: 

System specification

lingua: inglese 

Insegnamento: Specifica di sistemi

Anno di corso: II

CFU: 6

SSD: INF/01

Ore di lezione: 38

Ore di esercitazione: 10

Semestre: 2

Codice:

Obiettivi formativi:

Il corso si propone di fornire le nozioni di base per il problema della modellizzazione formale di sistemi Hardware e Software finalizzate alla verifica delle proprietà di correttezza. In particolare, il corso riguarderà la modellizzazione di sistemi a stati finiti o infiniti sia "chiusi" (non interagenti con l'ambiente) che "aperti"(interagenti con l'ambiente). Per i sistemi aperti, in particolare, verrà considerata come tecnica di modellazione la teoria dei giochi e il module checking. Si creerà dimestichezza con gli ambienti attualmente più evoluti di Model Checking.

Contenuti:

Introduzione ai fondamenti dei linguaggi di specifica e ai loro problemi decisionali: automi a stati finiti; autom su alberi; automi gerarchici; automi temporizzati.  Nozioni di teoria dei giochi per la verifica di sistemi interagenti con l'ambiente: giochi su sistemi a stati finiti; giochi con informazione parziale. Introduzione agli ambienti di verifica SPIN e NuSMV, e ai linguaggi di specifica adottati (Promela per SPIN). Introduzione ai linguaggi di specifica delle proprietà con particolare riguardo alle logiche temporali LTL (Linear Temporal Logic) CTL (Computation Tree Logic) ATL (Alternating Temporal Logic) ed SL (Strategy Logic). Il model checking. Studio di applicazioni in contesti AI multi agente.

Prerequisiti: Nessuno

Modalità didattiche:

Lezioni frontali. Esercitazioni.

Materiale didattico:

C. Baier, J. Katoen, Principles of model checking, The MIT Press

 

Modalità di esame:

L'esame si articola in prova

 

     

 

 

Solo orale

 

In caso di prova scritta i quesiti sono

 

           

 

Altro 

Sviluppo di un caso di studio

 

Docente : Murano Aniello