Předmět Formální specifikace systémů založených na počítačích (FIT-SSD)

Na serveru studentino.cz naleznete nejrůznější studijní materiály: zápisky z přednášek nebo cvičení, vzorové testy, seminární práce, domácí úkoly a další z předmětu FIT-SSD - Formální specifikace systémů založených na počítačích, Fakulta informačních technologií, Vysoké učení technické v Brně (VUT).

Materiál	Typ	Datum	Počet stažení

Cíl

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.

Osnova

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 Osnova ostatní - projekty, práce:Prostudování a zpracování formou eseje vybraného formálního aparátu automatů, algeber procesů, temporálních logik resp. teorie stop aplikovaného na problematiku řešenou v disertační práci studenta.

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

Požadavky

Základní přednášky matematiky na technických universitách

Garant

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

Vyučující

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