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 tramite la piattaforma e-learning
Periodo di erogazione dell'insegnamento
Secondo semestre
Modalità di verifica del profitto e valutazione
La verifica dell'apprendimento comprende una prova scritta e un colloquio orale.
Nella prova scritta si richiede di svolgere alcuni esercizi simili a quelli svolti a lezione e durante le esercitazioni e in laboratorio. L'obiettivo di valutazione della prova scritta consiste nel controllo della preparazione su alcuni argomenti fondamentali del programma d’esame, e nel controllo delle competenze di problem solving disciplinare.
Si è ammessi al colloquio orale se è stata superata la prova scritta
Al colloquio orale, oltre alla discussione dello scritto, vengono fatte domande sugli argomenti del corso. L'obiettivo del colloquio orale è valutare la capacità dello studente di esporre gli argomenti del corso, e di effettuare brevi ragionamenti su di essi.
La valutazione è complessiva e viene definita al colloquio orale.
Orario di ricevimento
Su appuntamento.
Sustainable Development Goals
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 on the e-learning platform
Semester
Second semester
Assessment method
The assessment method consists of written and oral examination
The written exam consists of some exercises, which are similar to the ones made in class during the lectures.
The evaluation objective of the written test consists in the control of the preparation on some fundamental topics of the exam program, and in the control of disciplinary problem solving skills.
The student is admitted to the oral exam if he/she has passed the written test
In the oral exam the solution of such exercises will be discussed and some questions on the developed arguments will be done.
The objective of the oral interview is to evaluate the student's ability to present the topics of the course, and to make brief thoughts on them.
The assessment is comprehensive and is defined in the oral interview.
Office hours
On appointment
