Detail předmětu

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

SSD Ak. rok 2003/2004 letní semestr

Aktuální akademický rok

Systémy založené na počítačích a jejich specifikace. Vybrané statě z prerekvisity. Principy algeber procesů. Příklady algeber procesů. Algebry procesů reálného času. Přehled temporálních logik. Pokročilé principy temporálních specifikací. Příklady temporálních logik reálného času. Vzájemné souvislosti dokazování a kontroly modelem. Algebry procesů a temporální logiky. Teorie stop a ostatní teorie. Vzájemné souvislosti. Případové studie.

Podrobněji ...

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.

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