Course Syllabus
Obiettivi
Alla fine del corso lo studente sarà in grado di modellare, a diversi livelli di astrazione, sistemi concorrenti o distribuiti costituiti da componenti che operano in modo indipendente e che interagiscono tra loro, 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
Viene introdotto un linguaggio logico per specificare le proprietà di comportamento di sistemi concorrenti; vengono presentate le reti di Petri come utile strumento per modellare tali sistemi e analizzarne le proprietà. Vengono introdotti algoritmi e strumenti software per tale modellazione e analisi.
Programma esteso
1. Panoramica dei metodi formali nella progettazione e analisi del software, in particolare nel caso di sistemi concorrenti.
2. Un linguaggio logico per specificare le proprietà di comportamento dei sistemi concorrenti: la logica proposizionale temporale lineare PLTL. Sintassi e semantica, equivalenza tra formule. Esempi di formule PLTL insoddisfacibili. Proprietà di liveness, di safety e di fairness in PLTL Sistemi di transizioni e model checking.
3. Linguaggi e strumenti software per la specifica e analisi dei sistemi e programmi concorrenti
4. Le Reti di Petri: fondamenti concettuali, applicazioni e tecniche di analisi: i sistemi elementari, la regola di scatto e il grafo dei casi raggiungibili. Reti Posti e Transizioni: matrice di incidenza, vettore di Parikh e l’equazione di stato. Proprietà di comportamento e loro verifica sul grafo di raggiugbilità. Analisi strutturale: S- e T-invarianti; sifoni e trappole; teoremi del rango. Sottoclassi particolari: macchine a stati, grafi marcati, reti Free-choice e verifica di proprietà su tali sottoclassi. Altre classi di reti.
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.
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.
Orario di ricevimento
Su appuntamento.
Aims
At the end of the course, the student will be able to model, at several levels of abstraction, concurrent systems done by interacting components 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
A logic language will be introduced to specify behavioral properties of concurrent systems. Petri nets will be presented as useful formal tools to model concurrent systems and to analyze their properties. Algorithms and software tools for the design and analysis of such systems will be also introduced.
Detailed program
1. Survey of formal methods in the design and analysis of concurrent systems.
2. A logic language to specify behavioral properties of concurrent systems: Propositional Linear Temporal Logic (PLTL), syntax and semantics, equivalence of formulas, examples of unsatisfiable formulas in PLTL, properties of liveness, safety and fairness in PLTL. Transition systems and model checking.
3. Languages and software tools to specify and analyse concurrent systems and programs.
4. Petri nets: conceptual foundation, applications, and analysis techniques: elementary net systems, transition rule, case graph. Place Transition nets: incidence matrix, Parikh vector, state equation. Behavioral properties and their verification on the reachability graph. Structural analysis: S- and T-invariants; siphons and traps; rank theorems. Net subclasses: state machines, marked graphs, Free-choice nets and analysis of behavioral properties on such subclasses. Other classes of nets.
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.
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.
Office hours
On appointment