FORMAL METHODS FOR SYSTEM VERIFICATION

Anno accademico

2019/2020 Programmi anni precedenti

Titolo corso in inglese

FORMAL METHODS FOR SYSTEM VERIFICATION

Codice insegnamento

CM0474 (AF:306545 AR:166113)

Modalità

In presenza

Crediti formativi universitari

6

Livello laurea

Laurea magistrale (DM270)

Settore scientifico disciplinare

INF/01

Periodo

I Semestre

Anno corso

1

Sede

VENEZIA

Spazio Moodle

Link allo spazio del corso

Inquadramento dell'insegnamento nel percorso del corso di studio

Il corso si propone di fornire le basi teoriche per l'utilizzo di strumenti formali di modellazione, analisi e verifica sia di software che di sistemi informatici complessi.
Il corso presenta i principali strumenti formali per specificare ed analizzare il comportamento di un sistema di processi che interagiscono fra di loro con particolare attenzione all'analisi delle prestazioni.
In particolare verrà introdotto un calcolo stocastico che consente di descrivere ed analizzare il comportamento dinamico di sistemi distribuiti e concorrenti.

Risultati di apprendimento attesi

Lo studente acquisirà conoscenze e competenze sugli aspetti fondamentali da considerare nella progettazione di software con requisiti di affidabilità e prestazioni.
In particolare, acquisirà conoscenze sui metodi formali per la verifica e la valutazione delle prestazioni di sistemi concorrenti e distribuiti.
Saprà inoltre utilizzare gli strumenti formali e le metodologie per la modellazione dei sistemi, così come le tecniche per la progettazione e l'analisi di software e sistemi che soddisfino determinati requisiti di affidabilità e prestazioni.

Prerequisiti

E' richiesta una conoscenza di base di matematica e del calcolo delle probabilità.

Contenuti

Verrà introdotta l'algebra dei processi, stocastica, detta PEPA (acronimo di: Performance Evaluation Process Algebra) e verranno presentate alcune tecniche di analisi delle prestazioni.
- Il linguaggio PEPA: sintassi e semantica.
- Distribuzione stazionaria.
- Metodi di aggegazione e relazioni di equivalenza.
- Forme prodotto.
- Applicazioni all'analisi delle prestazioni.

Testi di riferimento

- J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996. http://www.dcs.ed.ac.uk/pepa/book.pdf
- Articoli forniti dal docente.

Modalità di verifica dell'apprendimento

L'esame può essere svolto in due modi:
- svolgendo un progetto di modellazione e analisi di un semplice sistema informatico e sostenendo una prova orale sul progetto e sul programma del corso allo scopo di verificare le competenze e capacità dello studente nell'applicare le conoscenze apprese durante il corso
oppure
- svolgendo una prova scritta nelle date degli appelli. La prova scritta consiste in esercizi di modellazione e analisi di semplici sistemi informatici allo scopo di verificare le competenze e capacità dello studente nell'applicare le conoscenze apprese durante il corso.

Metodi didattici

Lezioni teoriche ed esercizi svolti alla lavagna.

Lingua di insegnamento

Inglese

Modalità di esame

scritto

Obiettivi Agenda 2030 per lo sviluppo sostenibile

Questo insegnamento tratta argomenti connessi alla macroarea "Città, infrastrutture e capitale sociale" e concorre alla realizzazione dei relativi obiettivi ONU dell'Agenda 2030 per lo Sviluppo Sostenibile

Programma definitivo.

Data ultima modifica programma: 17/09/2019