FORMAL METHODS FOR SYSTEM VERIFICATION

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.

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.

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

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.

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

L’esame può essere sostenuto in due modi:
1) Una prova scritta con la possibilità di una prova orale integrativa, se ritenuto necessario dalla docente o su richiesta dello studente. La prova scritta consiste in domande aperte sugli argomenti del corso ed esercizi. L'orale viene svolto solo se la prova scritta è risultata sufficiente. In caso di esito negativo dell'orale, sarà necessario ripetere lo scritto.
2) Un progetto da presentare alla fine delle lezioni e una prova orale. La prova orale prevede la discussione del progetto, lo svolgimento di esercizi prendendo spunto dal tema del progetto e domande aperte sugli argomenti del corso.

Descrizione della prova d'esame:
La prova d'esame, sia essa nella forma di una prova scritta o un progetto con prova orale, ha l’obiettivo di valutare le competenze di problem solving dello studente, la conoscenza dei concetti fondamentali, e la capacità di risolvere esercizi e dimostrare teoremi. Consiste in esercizi e domande a risposta aperta riguardanti i principali argomenti trattati nel corso.
La prova scritta può essere seguita da una prova orale, qualora la docente lo ritenga opportuno o lo studente desideri integrare l’esito. La prova orale viene svolta solo se la prova scritta è risultata sufficiente. In caso di esito negativo dell'orale, sarà necessario ripetere lo scritto.

scritto

Il/la docente ha il dovere di vigilare affinché siano rispettate le regole di autenticità e originalità delle prove d'esame. Di conseguenza, nei casi in cui vi sia il sospetto di un comportamento irregolare, l'esame può prevedere un ulteriore approfondimento, contestuale alla prova d'esame, che potrà essere realizzato anche in modalità differente rispetto alle modalità sopra riportate.

La valutazione dell'esame sarà così articolata: qualità degli elaborati (prova scritta o progetto): 30%, capacità di esporre, in forma scritta o orale, i concetti fondamentali della disciplina: 30%, capacità di risolvere problemi applicando le tecniche illustrate durante il corso: 40%.

Lezioni teoriche ed esercizi svolti alla lavagna.

Sostenibilità:

Insegnamento sostenibile
Dispense e materiali di approfondimento disponibili online; testi di riferimento in formato e-book
Forum virtuali
Piattaforme e-learning, moodle

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