Detail předmětu

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

SSD Ak. rok 2011/2012 letní semestr

Aktuální akademický rok

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.

Garant předmětu

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

Jazyk výuky

česky

Zakončení

zkouška

Rozsah

  • 39 hod. přednášky

Zajišťuje ústav

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

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ů.

Kontrolovaná výuka

Zpracovaní a obhájení eseje.

Nahoru