Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail předmětu
FIT-SSDAk. rok: 2015/2016
Cílem tohoto předmětu je nabídnout přehled typických formálních nástrojů využitelných pro specifikace chování systémů založených na počítačích a komponent těchto systémů. Po absolvování přehledu každý student zvolí vhodný nástroj aplikovatelný v rámci tématu jeho disertace a prostuduje jej podrobněji. Přehled pokryje podoblasti s následujícími příklady nástrojů a metod: Konečné automaty, omega-automaty, časované automaty. Principy algeber procesů, BPA. Příklady algeber procesů: CSP, CCS. Algebry časovaných procesů, TCSP. Přehled temporálních logik. Temporální specifikace vlastností typu: dosažitelnost, bezpečnost, živost, spravedlivost, odezva v omezeném čase, ... . Příklady temporálních logik reálného času. Vzájemné souvislosti dokazování a kontroly modelu. Algebry procesů a temporální logiky. Teorie stop a ostatní teorie. Vzájemné souvislosti. Případové studie.
Otázky k SDZ:
Jazyk výuky
Počet kreditů
Garant předmětu
Zajišťuje ústav
Výsledky učení předmětu
Prerekvizity
Způsob a kritéria hodnocení
Osnovy výuky
Učební cíle
Vymezení kontrolované výuky a způsob jejího provádění a formy nahrazování zameškané výuky
Základní literatura
Doporučená literatura
Zařazení předmětu ve studijních plánech
obor DVI4 , libovolný ročník, letní semestr, volitelný
Přednáška
Vyučující / Lektor
Osnova