Course Syllabus
Obiettivi
Alla fine del corso lo studente sarà in grado di modellare, a diversi livelli di astrazione, sistemi concorrenti semplici ma non banali e di descriverne i requisiti per mezzo di un linguaggio logico; conoscerà le tecniche per verificarne le proprietà di comportamento; saprà usare alcuni strumenti software per il disegno e l'analisi di sistemi concorrenti.
Contenuti sintetici
Ruolo e limiti dei metodi formali nella progettazione e nell'analisi del software, particolarmente nel caso di sistemi concorrenti; tecniche per definire la semantica di programmi e sistemi concorrenti; strumenti formali per specificare sistemi concorrenti, i loro requisiti e le loro proprietà; algoritmi e strumenti software per il disegno e l'analisi di sistemi concorrenti. In particolare si introdurrà la teoria delle reti di Petri.
Programma esteso
1. Panoramica dei metodi formali nell'informatica. Sistemi e programmi concorrenti.
2. Strumenti per la modellazione di sistemi concorrenti: stemi di transizioni e altre notazioni formali.
3 Analisi di sistemi concorrenti: proprietà di liveness e di safety, logiche modali e temporali, model checking
4 Reti di Petri: fondamenti concettuali, applicazioni, varianti, tecniche di analisi.
5 Teoria dei sistemi: nozioni di base dei sistemi dinamici, cenni al modello degli automi cellulari
Prerequisiti
Nozioni di base di logica proposizionale. Nozioni di base di analisi matematica e di matematica discreta (come trattata nel corso di fondamenti dell'nformatica).
Modalità didattica
Lezioni ed esercitazioni in aula. Esercitazioni in laboratorio. Il corso è erogato in italiano.
Se dovesse esserci ancora l'emergenza Covid-19 lezioni, esercitazioni e laboratori saranno videoregistrate e trasmesse in parte in modalità asincrona e in parte in modalità sincrona.
Materiale didattico
Dispense e articoli monografici forniti dal docente.
Periodo di erogazione dell'insegnamento
Secondo semestre
Modalità di verifica del profitto e valutazione
L'esame consiste in uno scritto e in un orale.
Lo scritto consiste nello svolgimento di alcuni esercizi.
Al colloquio orale, oltre a discutere la soluzione degli esercizi dello scritto, verranno fatte domande sugli argomenti sviluppati e potrà essere discussa la soluzione di alcuni esercizi di modellazione e di verifica di proprietà svolti in laboratorio durante il corso. Il testo di tali esercizi sarà a disposizione sul sito del corso.
La valutazione è complessiva e viene definita al colloquio orale.
Se ci sarà ancora emergenza Covid-19 gli esami orali saranno solo telematici. Verranno svolti utilizzando la piattaforma WebEx o google.meet e nella pagina e-learning dell'insegnamento verrà riportato un link pubblico per l'accesso all'esame di possibili spettatori virtuali.
Orario di ricevimento
Su appuntamento.
Aims
At the end of the course, the student will be able to model, at several levels of abstraction, simple concurrent systems and to specify their requirements by means of a logic; the student will know the main techniques to prove the system's behavioral properties, and will be able to use some software tools for the design and analysis of concurrent systems.
Contents
Role and scope of formal methods in software design and analysis, particularly for concurrent systems. Techniques for defining the semantics of concurrent programs and systems; formal tools for specifying concurrent systems, requirements and properties; algorithms and software tools for the design and analysis of concurrent systems. In particular, the theoru of Petri nets will be introduced.
Detailed program
1 Survey of formal methods in computer science. Concurrent systems and programs.
2 Modeling tools for concurrent systems: transition systems, other formal notations.
3 Analysis of concurrent systems: liveness and safety properties, modal and temporal logics, model checking.
4 Petri nets: conceptual foundation, applications, types, analysis techniques.
5 Theory of systems: basic notions of dynamical systems and cellular automata.
Prerequisites
Basic notions of propositional logic. Basic notions of mathematical analysis and of discrete mathematics (as presented in the course of Fundamentals of Computer Science).
Teaching form
Lectures, practical exercises, laboratory activity. Language: Italian.
If there will be Covid emergency, the teaching activity will be online or recorded.
Textbook and teaching resource
Handouts, research and survey papers.
Semester
Second semester
Assessment method
Written and oral exam. The written exam consists in the execution of some exercises. In the oral exam the solution of such exercises will be discussed and some questions on the developed arguments will be done. Moreover, the solution of some exercises on modeling and verification developed during the lab could be also discussed.
No score is given to the written exam, the score is defined at the interview.
If there will be Covid-19 emergency, the oral exam esami will be online on WebEx or google.meet and in the e-learning page there will be the public link.
Office hours
On appointment