Detail předmětu

Formální specifikace systémů založených na počítačích

FIT-SSDAk. rok: 2010/2011

Jazyk výuky

čeština

Počet kreditů

Garant předmětu

Zajišťuje ústav

Základní literatura

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.

Doporučená literatura

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.

Zařazení předmětu ve studijních plánech

Program VTI-DR-4 doktorský
obor DVI4 , libovolný ročník, letní semestr, volitelný
Program VTI-DR-4 doktorský
obor DVI4 , libovolný ročník, letní semestr, volitelný

Přednáška

39 hod., nepovinná

Vyučující / Lektor

Osnova

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

VUT