Detail předmětu

Komunikace v počítačových aplikacích

KPA Ak. rok 2006/2007 letní semestr 5 kreditů

Aktuální akademický rok

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. Protoly pro reálný čas. Návrh aplikací.

Garant předmětu

Švéda Miroslav, prof. Ing., CSc.

Jazyk výuky

česky

Zakončení

zkouška

Rozsah

  • 39 hod. přednášky
  • 2 hod. laboratoře
  • 4 hod. pc laboratoře
  • 7 hod. projekty

Zajišťuje ústav

Ústav informačních systémů (UIFS)

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

Výroková logika. Základy predikátové logiky 1. řádu. Základní pojmy komunikačních protokolů.

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

Nahoru