- Concurrent Models
- Summary
Course Syllabus
Obiettivi
Acquisire la capacità di modellare e analizzare formalmente sistemi concorrenti; acquisire la capacità di esprimere in linguaggi logici proprietà dei sistemi concorrenti.
Contenuti sintetici
Strumenti teorici per comprendere e manipolare concetti di base dell'informatica relativi al comportamento e alla descrizione di processi distribuiti e concorrenti. Nozioni fondamentali per la verifica di proprietà di programmi e di modelli di sistemi.
Programma esteso
- Modelli formali per la specifica e la verifica di correttezza dei programmi. La
semantica assiomatica dei programmi sequenziali, la logica di Hoare; dimostrazioni di correttezza di programmi sequenziali. - Modelli della concorrenza: modelli di sistemi reattivi, calcoli di
processi (CCS, Calculus of Communicating Systems) e reti di Petri. - Semantica interleaving (sistemi di transizioni) e a ordini
parziali (reti di Petri) di sistemi concorrenti. Semantica osservazionale, nozioni di equivalenza fra processi, bisimulazione. - La specifica di proprietà e la loro verifica (logiche modali e temporali, algoritmi di model-checking). Linear Temporal Logic (LTL), Computation Tree Logic (CTL), cenni al calcolo mu.
Prerequisiti
Nozioni di base di programmazione imperativa; nozioni di base di logica proposizionale.
Modalità didattica
Corso erogato in italiano. Lezioni frontali (3 CFU, 24 ore) e esercitazioni in aula (3 CFU, 30 ore).
Nel periodo di emergenza Covid-19 le lezioni si svolgeranno in modalità mista: parziale presenza e lezioni videoregistrate, con periodici incontri in videoconferenza.
Materiale didattico
Dispense e articoli pubblicati sul sito dell'insegnamento. Testi di consultazione indicati sul sito dell'insegnamento.
Periodo di erogazione dell'insegnamento
Primo semestre
Modalità di verifica del profitto e valutazione
La valutazione di questo modulo comprende una prova scritta con esercizi su tutte le parti del programma, e un colloquio, con discussione della prova scritta e domande sugli argomenti del modulo. La valutazione è complessiva e definita dopo il colloquio.
Nel periodo di emergenza Covid-19 gli esami potranno svolgersi in forma telematica, utilizzando le piattaforme disponibili; nella pagina e-learning
dell'insegnamento verrà riportato un link pubblico per l'accesso all'esame
di possibili spettatori virtuali.
Orario di ricevimento
Luca Bernardinello: martedì dalle 10:30 alle 12:00, o per appuntamento.
Lucia Pomello: martedì dalle 14.00 alle 16.00 o per appuntamento.
Aims
Acquire the ability to formally model and analyze concurrent systems; acquire the ability to state properties of concurrent systems by means of temporal logics.
Contents
Theoretical tools useful to understand and manipulate basic notions of computer science, related to the behaviour and the specification of distributed and concurrent processes. Fundamental notions about verifying properties of programs ans models of systems.
Detailed program
- Formal models for specifying and verifying the correctness of programs. Axiomatic semantics of sequential programs, Hoare logic; proofs of correctness of sequential programs.
- Models of concurrency: models of reactive systems, process calculi (CCS, Calculus of Communicating Systems), Petri nets.
- Interleaving semantics (transition systems) of concurrent systems; partial order semantics (Petri nets). Semantics based on observation, equivalence notions for processes, bisimulation.
- Specification and verification of properties (modal and temporal logics, algorithms for model-checking). Linear Temporal Logic (LTL), Computation Tree Logic (CTL), basic notions of the mu-calculus.
Prerequisites
Basic notions of imperative programming; basic notions of propositional logic.
Teaching form
In Italian language. Lectures (3 CFU, 24 hours) and practice sessions (3 CFU, 30 hours).
During the Covid-19 emergency, lectures will take place partly in the classroom, partly as recorded lectures, with periodic meetings as videoconference.
Textbook and teaching resource
Notes and papers available on the course site. Reference texts suggested on the course site.
Semester
First semester.
Assessment method
The evaluation for this module includes a written exam with assignments on all sections of the programme, and an oral exam, with discussion of the written part, and questions on the subjects of the module. The score is defined after the discussion.
During the Covid-19 emergency, exams will take place online, using the available platforms; a public link will be published on the site of the course, thus allowing attending the exams.
Office hours
Luca Bernardinello: Tuesday 10:30 - 12:00, or on appointment.
Lucia Pomello: Tuesday 14:00 - 16:00, or on appointment.