Komunikační protokoly

Garant předmětu:

Přednášející:

Cvičící:

Předmět zajišťuje:

katedra počítačových systémů

Anotace:

Studenti porozumí trendům vývoje moderních komunikačních protokolů, architekturám vybraných distribuovaných systémů a formálním nástrojům pro jejich popis, modelování a verifikaci.

Požadavky:

Osnova přednášek:

1.Principy moderních komunikačních protokolů.

2.Automatový popis protokolu, aplikace metod ověřování distribuovaných mechanismů.

3.Využití atributových gramatik, systém RTAG.

4.Prototypový systém Promela a ESTELLE.

5.Systém SPIN založený na postupu Promela.

6.Specifikační jazyk LOTOS.

7.Algoritmy validace a verifikace protokolu.

8.Rozšíření SPIN na model checking.

9.Protokolové transformace.

10.Dynamické chování síťových protokolů při záteži.

Osnova cvičení:

Cíle studia:

Mechanismy ochrany proti chybám v komunikačních protokolech vedly k vytvoření systému oveřování odolnosti, v současnosti mají úzkou vazbu na implementaci mechanismu ověřování odolnosti distribuovaných aplikací.

Cílem předmětu je uvést studenty do tohoto kontextu rozvoje moderních komunikačních protokolů.

Studijní materiály:

Holzmann G.J.: Design and Validation of Computer Protocols. Prentice Hall 1998

Ben-Ari M.. Principles of the SPIN Model Checker, Springer 2008.

Poznámka:

Další informace:

Pro tento předmět se rozvrh nepřipravuje

Předmět je součástí následujících studijních plánů:

• Informatika (doktorská) (povinně volitelný předmět)
• Informatika (povinně volitelný předmět)