Detail předmětu
Formální specifikace systémů založených na počítačích
SSD Ak. rok 2013/2014 letní semestr
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:
- Diskrétní systém a stavový model jeho chování
- Metody verifikace teorémů v predikátové logice
- Formální modely vycházející z konečných automatů
- Temporální logiky LTL a CTL - principy
- Procesní algebra CSP - principy
- Čas ve formálních modelech - příklady
- Specifikace vlastností typu: dosažitelnost, bezpečnost, živost, spravedlivost, odezva v omezeném čase
- Verifikace konkrétních vlastností ve formálních modelech
- Příklad nástroje typu model-checker
- Problémy formálních specifikací reálných aplikací a přístupy k jejich řešení
Garant předmětu
Jazyk výuky
Zakončení
Rozsah
- 39 hod. přednášky
Zajišťuje ústav
Získané dovednosti, znalosti a kompetence z předmětu
Informovanost o principech formálních specifikací a o současném stavu jejich uplatnění při návrhu systémů založených na počítačích.
Cíle předmětu
Být informován o principech formálních specifikací a jejich uplatnění při návrhu systémů založených na počítačích a jejich komponent.
Požadované prerekvizitní znalosti a dovednosti
Základní přednášky matematiky na technických universitách
Literatura studijní
- Kreowski H.-J., Montanari U., Orejas F., Rozenberg G., Taentzer G.: Formal Methods in Software and Systems Modeling. Springer, LNCS 3393, 2005.
- Berard B. et al.: Systems and Software Verification. Springer-Verlag, 2001.
- Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
- Schneider K.: Verification of Reactive Systems. Springer-Verlag, 2004.
- Abramsky S., Gabbay D.M., Maibaum T.S.E. (Editors): Handbook of Logic in Computer Science. Volumes 1, 2, 3, 4, 5. Oxford Science Publications, 2000.
- de Bakker J.W., de Roever W.-P., Rozenberg G. (Editors): Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. Springer-Verlag, LNCS 354, 1989.
- Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. Springer-Verlag, LNCS 827, 1994.
- Huth M.R.A., Ryan M.D.: Logic in Computer Science -- Modelling and Reasoning about Systems. Cambridge University Press, 2002.
Literatura referenční
- Berard B. et al.: Systems and Software Verification. Springer-Verlag, 2001.
- Clarke E.M., Jr., Grumberg O., Peled D.A.: Model Checking. MIT Press, 2000.
- Schneider K.: Verification of Reactive Systems. Springer-Verlag, 2004.
- de Bakker J.W., de Roever W.-P., Rozenberg G. (Editors): Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. Springer-Verlag, LNCS 354, 1989.
- Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. Springer-Verlag, LNCS 827, 1994.
- Huth M.R.A., Ryan M.D.: Logic in Computer Science -- Modelling and Reasoning about Systems. Cambridge University Press, 2002.
Osnova přednášek
- Systémy založené na počítačích a jejich specifikace
- Konečné automaty, omega-automaty, časované automaty
- Principy algeber procesů, BPA; příklady algeber procesů, CSP, CCS
- Algebry procesů reálného času, 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; TLA jako logika reálného času
- Dokazování
- Kontrola modelu
- Algebry procesů a temporální logiky
- Teorie stop
- Vzájemné souvislosti
- Případové studie
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ů.
Metody vyučování
Výuka předmětu je realizována formou: Přednáška - 3 vyučovací hodiny týdně.
Kontrolovaná výuka
Zpracovaní a obhájení eseje.
Zařazení předmětu ve studijních plánech