Předmět Specifikace vestavěných systémů (v angličtině) (FIT-SVSe)

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-SVSe - Specifikace vestavěných systémů (v angličtině), Fakulta informačních technologií, Vysoké učení technické v Brně (VUT).

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

Cíl

Porozumět principům formálních specifikací a jejich uplatnění při návrhu vestavěných systémů; být informován o využití temporální logiky pro modelování reaktivních systémů a systémů pracujících v reálném čase; být informován o architekturách vestavěných distribuovaných systémů.

Osnova

Osnova přednášek:Principy návrhu vestavěných distribuovaných systémů Modely reaktivních systémů a systémů pracujících v reálném čase Spravedlivost, živost, bezpečnost, realizovatelnost; živost reálného času Základy temporální logiky Časové modely a temporální logiky Temporální logika a reálný čas Formální specifikace vestavěných systémů Dokazovací systémy Kontrola modelem Verifikace systémů pracujících v reálném čase Formální specifikace abstraktních datových struktur a objektů, algebraické specifikace Použití systémů teorie typů pro specifikaci a ověření programůOsnova numerických cvičení:Představení systému Coq - stručné vysvětlení použitého formalismu nástroje, představení příkazového jazyka nástroje, demonstrace základních konkstrukcí jazyka a ukázka specifikace a ověření vlastností jednoduchého algoritmuOsnova laboratorních cvičení:Správa vestavěné aplikace z intranetu Osnova počítačových cvičení:Úvodní sezenámení se systémem Coq, specifikace jednoduchých vlastností Základní techniky specifikace programů Ověřování správnosti jednoduchého algoritmuOsnova ostatní - projekty, práce:Formální specifikace a verifikace vlastností vestavěného systému

Literatura

Huth, M.R.A., Ryan, M.D.: Logic in Computer Science - Modelling and Reasoning about Systems, Cambridge University Press, 2002, ISBN 0-521-65602-8 Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000, ISBN 0-262-03270-8 de Bakker, J.W. et all. (Editors): Real-Time: Theory in Practice, Springer-Verlag, LNCS 600, 1992, ISBN 3-540-55564-1Schneider, K.: Verification of Reactive Systems, Springer-Verlag, 2004, ISBN 3-540-00296-0 Huth, M.R.A., Ryan, M.D.: Logic in Computer Science - Modelling and Reasoning about Systems, Cambridge University Press, 2002, ISBN 0-521-65602-8 Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000, ISBN 0-262-03270-8 de Bakker, J.W. et all. (Editors): Real-Time: Theory in Practice, Springer-Verlag, LNCS 600, 1992, ISBN 3-540-55564-1 Gabbay, D.M., Ohlbach, H.J. (Editors): Temporal Logic, Springer-Verlag, LNCS 827, 1994, ISBN 3-540-58241-X Monin, J.F., Hinchey, M.G.:Understanding Formal Methods, Springer-Verlang, 2003. Peled, D.A.:Software Reliability Methods, Text in Computer Science, Springer, 2001. Tennent, R.D.:Specifying Software: A Hand-On Introduction, Cambridge University Press, 2002. Bertot, Y., Casteran, P.:Interactive Theorem Proving and Program Development, Springer-Verlang, 2004.

Požadavky

Výroková logika. Základy predikátové logiky 1. řádu. Základní pojmy komunikačních protokolů.

Garant

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

Vyučující

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