66870 - MODELLI E SISTEMI CONCORRENTI

Scheda insegnamento

  • Docente Roberto Gorrieri

  • Crediti formativi 6

  • SSD INF/01

  • Modalità di erogazione In presenza (Convenzionale)

  • Lingua di insegnamento Italiano

Anno Accademico 2017/2018

Conoscenze e abilità da conseguire

Al termine del corso, lo studente conosce i paradigmi di base della concorrenza, i loro modelli ed i sistemi di verifica di proprietà di tali modelli. È in grado di analizzare semplici programmi concorrenti con strumenti automatici o semi-automatici.

Programma/Contenuti

- Introduzione alla concorrenza e al problema della correttezza del progetto di sistemi reattivi.

- Sistemi di transizione etichettati.

- Equivalenze comportamentali: tracce, simulazione, bisimulazione forte e debole, proprietà.

- Il linguaggio CCS: semantica operazionale strutturata.

- Sottoclassi di CCS: processi finiti, processi a stati finiti, processi regolari, BPP, processi a rete finita, CCS finitario.

- Turing completezza di CCS finitario; indecidibilità delle equivalenze comportamentali per CCS finitario.

- Cenni a CCS value-passing.

- Proprieta' algebriche, congruenze comportamentali e cenni alle assiomatizzazioni. 

- Espressività di CCS: implementabilità di operatori aggiuntivi (scelta interna, hiding, composizione sequenziale) 

- Problema della sincronizzazione muti-way: Multi-CCS; caso di studio: filosofi a cena.

- Reti di Petri: definizione, equivalenze comportamentali, proprietà decidibili, espressività.

- Cenni ai linguaggi per rappresentare reti di Petri. Computabilità distribuita.

- Teoria del punto fisso, minimi e massimi punti fissi, equivalenza forte come massimo punto fisso.

- Logica di Hennessy-Milner (HML), estensione con formule definite in modo ricorsivo, modal mu-calculus.
- Tool di analisi e verifica per CCS e HML: Concurrency Workbench (CWB).
- Modellazione, analisi e verifica di alcuni algoritmi di mutua esclusione con CWB.


Testi/Bibliografia

R. Gorrieri, C. Versari

Introduction to Concurrency Theory: Transition Systems and CCS

EATCS texts in theoretical computer science, Springer, 2015.

 

L. Aceto, A. Ingolfsdottir, K.G. Larsen, J. Srba

Reactive Systems: Modelling, Specification and Verification

Cambridge University Press, 2007

 

R. Gorrieri

Process Algebras for Petri Nets: The Alphabetization of Distributed Systems, EATCS monographs in theoretical computer science, Springer, 2017

 

Modalità di verifica dell'apprendimento

Prova scritta ed esame orale

Strumenti a supporto della didattica

Lezioni frontali con proiettore.

Link ad altre eventuali informazioni

http://www.cs.unibo.it/~gorrieri/MSC/msc.html

Orario di ricevimento

Consulta il sito web di Roberto Gorrieri