IV010 Komunikace a paralelismus

Fakulta informatiky
jaro 2023
Rozsah
2/0. 2 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: z.
Vyučující
prof. RNDr. Luboš Brim, CSc. (přednášející)
Garance
prof. RNDr. Luboš Brim, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Luboš Brim, CSc.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
St 15. 2. až St 10. 5. St 12:00–13:50 B410
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 82 mateřských oborů, zobrazit
Cíle předmětu
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 a orientovat se v nejčastějších typech ekvivalencí mezi procesy a jejich omezení.
Výstupy z učení
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 a orientovat se v nejčastějších typech ekvivalencí mezi procesy a jejich omezení. Cíle předmětu anglicky
Osnova
  • 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.
  • Temporální vlastnosti procesů.
Literatura
  • MILNER, Robin. Communicating and mobile systems : the Pi calculus. Cambridge: Cambridge University Press, 1999, xii, 161 s. ISBN 0-521-64320-1. info
  • MILNER, Robin. Communication and concurrency. New York: Prentice Hall, 1989, 260 s. ISBN 0-13-115007-3. info
Výukové metody
přednášky, domácí úkoly
Metody hodnocení
Zkouška je písemná. Při zadání průběžných testů během semestru, mají tyto podíl nejvýše 30% na závěrečném hodnocení. Pomocné materiály nejsou povoleny.
Navazující předměty
Informace učitele
https://www.fi.muni.cz/usr/brim/home/#teaching
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích podzim 2002, jaro 2003, jaro 2004, jaro 2005, jaro 2006, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2022, jaro 2024.