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

Zápočet není ustanoven.

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

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

• Správa vestavěné aplikace z intranetu

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

• Formální specifikace a verifikace vlastností vestavěného systému

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

• 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

• Program IT-MGR-2 magisterský navazující

  obor MBS , libovolný ročník, letní semestr, povinně volitelný
  obor MBI , libovolný ročník, letní semestr, volitelný
  obor MIS , libovolný ročník, letní semestr, povinně volitelný
  obor MIN , libovolný ročník, letní semestr, volitelný
  obor MMI , libovolný ročník, letní semestr, povinně volitelný
  obor MMM , libovolný ročník, letní semestr, volitelný
  obor MGM , libovolný ročník, letní semestr, volitelný
  obor MPV , libovolný ročník, letní semestr, volitelný
  

• Program IT-MGR-1H magisterský navazující

  obor MGH , libovolný ročník, letní semestr, doporučený
  

• Program IT-MGR-2 magisterský navazující

  obor MSK , 2. ročník, letní semestr, povinně volitelný