Specifikace vestavěných systémů (v angličtině)

• 39 hod. přednášky
• 6 hod. pc laboratoře
• 7 hod. projekty

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

Seznámení se se základy temporální logiky.

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

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

• 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
• Peregrin, J.: Logika a logiky, Academia, 2004, ISBN 80-200-1187-0

• Schneider, 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.

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

• Úvodní sezenámení se systémem Coq, specifikace jednoduchých vlastností
• Základní techniky specifikace programů
• Ověřování správnosti jednoduchého algoritmu

Hodnocení studia je založeno na bodovacím systému. Pro úspěšné absolvování předmětu je nutno dosáhnout 50 bodů.

Zápočet není ustanoven.

Metody vyučování závisí na způsobu výuky a jsou popsány článkem 7 Studijního a zkušebního řádu VUT.

Kontrolovanou výukou jsou domácí úkol/projekt, půlsemestrální zkouška a závěrečná zkouška. Půlsemestrální zkouška nemá náhradní termín. Závěrečná zkouška má dva náhradní termíny.