IV010 Komunikace a paralelismus
Cílem předmětu je získat základní dovednosti, které jsou používány pro formální specifikaci a analýzu komunikujících systémů, včetně teoretických základů příslušných formálních nástrojů. Po absolvování kurzu získají studenti schopnost specifikovat a implementovat v jazyce CCS jednoduché komunikační protokoly; analyzovat a formálně ověřovat korektnost návrhu; orientovat se v nejčastějších typech ekvivalencí mezi procesy a jejich omezení.
Rozvrh
Čtvrtek, 12:00 - 13:50, posluchárna B410Osnova
- Přehled modelů souběžných systémů. Modelování komunikace. Komunikační media, příklady komunikujících systémů, ekvivalence procesů.
- Jazyk CCS. Synchronizace, akce a přechody, vnitřní akce, sémantika, synchronizační stromy, předávání hodnot, rekurze a indukce.
- Rovnostní zákony a jejich aplikace. Klasifikace kombinátorů a zákonů, dynamické zákony, expanzní věta, statické zákony.
- Bisimulace a ekvivalence. Silná bisimulace a její vlastnosti, silná kongruence, bisimulace a její vlastnosti, dokazování správnosti komunikujícího systému.
- Teorie kongruence vzhledem k~pozorování. Experiment, rovnosti a jejich vlastnosti, řešení rovností, konečné procesy.
- Pi-kalkul. Modelování mobilních procesů, polyadický Pi-kalkul, příklady aplikací, redukce na lamba-kalkul.
Požadavky na absolvování předmětu
Předmět je zakončen písemnou zkouškou. Použití literatury a poznámek není při písemce povoleno.Doporučená literatura
- Milner, Robin. Communication and concurrency. Prentice Hall, 1989.
- Milner, Robin. Communicating and mobile systems : the Pi calculus. Cambridge University Press, 1999.
- L. Aceto, A. Ingolfsdottir, K. G. Larsen, J. Srba. Reactive Systems: Modelling, Specification and Verification.. Cambridge University Press, 2007.
- Učební text k přednáškám. (Materiály jsou dostupné pouze z domény .muni.cz)