Detail předmětu
Komunikace v počítačových aplikacích
KPA Ak. rok 2004/2005 zimní semestr 6 kreditů
Distribuované systémy pracující v reálném čase. Modely systémů diskrétních událostí a reálného času. Temporální logika. Formální specifikace a verifikace. Dokazovací systémy. Kontrola modelem. Protokoly pro reálný čas. Návrh aplikací.
Garant předmětu
Jazyk výuky
Zakončení
Rozsah
- 39 hod. přednášky
- 12 hod. pc laboratoře
- 14 hod. projekty
Zajišťuje ústav
Získané dovednosti, znalosti a kompetence z předmětu
Porozumění základním koncepcím a principům formálních specifikací reaktivních systémů a systémů pracujících v reálném čase.
Cíle předmětu
Seznámit se s principy formálních specifikací pro modelování reaktivních systémů a systémů pracujících v reálném čase; být informován o komunikačních protokolech pro reálný čas.
Požadované prerekvizitní znalosti a dovednosti
Nejsou žádné prerekvizity.
Literatura studijní
- de Bakker J.W. et all. (Editors): Real-Time: Theory in Practice. Springer-Verlag, LNCS 600, 1992.
Literatura referenční
- de Bakker J.W. et all. (Editors): Real-Time: Theory in Practice. Springer-Verlag, LNCS 600, 1992.
Osnova přednášek
- Úvod.
- Principy návrhu distribuovaných systémů.
- Distribuované systémy pracující v reálném čase.
- Modely systémů diskrétních událostí a systémů reálného času.
- Živost, bezpečnost, spravedlivost. Živost reálného času.
- Úvod do temporální logiky.
- Temporální logika a reálný čas.
- Formální specifikace a dokazovací systémy.
- Formální specifikace a kontrola modelem.
- Protokoly typu Fieldbus.
- Internet a aplikace pracující v reálném čase.
- Návrh distribuovaných aplikací.
- Případové studie.
Osnova počítačových cvičení
- Spin a Promela
- Simulace algoritmu ve Spinu
- Kontrola modelem
- Protokoly úrovně Fieldbus
- CANalyzer
- Intranet a CANalyzer
Průběžná kontrola studia
Hodnocení studia je založeno na bodovacím systému. Pro úspěšné absolvování předmětu je nutno dosáhnout 50 bodů.
Kontrolovaná výuka
Vypracování 2 projektů, absolvování polosemestrální písemné zkoušky