Detail předmětu

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

FIT-SVSeAk. rok: 2013/2014

Principy návrhu vestavěných distribuovaných systémů. Reaktivní systémy a systémy pracující v reálném čase. 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ů. Hybridní systémy. Dokazovací systémy. Kontrola modelem. Verifikace systémů pracujících v reálném čase.

Jazyk výuky

angličtina

Počet kreditů

5

Garant předmětu

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

Zajišťuje ústav

Ústav informačních systémů (UIFS)

Výsledky učení předmětu

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.

Prerekvizity

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

Plánované vzdělávací činnosti a výukové metody

Výuka předmětu je realizována formou: Přednáška - 3 vyučovací hodiny týdně, Cvičení na poč. - 1 vyučovací hodina týdně, Projekty - 1 vyučovací hodina týdně.

Způsob a kritéria hodnocení

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.

Osnovy výuky

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

Učební cíle

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

Vymezení kontrolované výuky a způsob jejího provádění a formy nahrazování zameškané výuky

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. 

Základní literatura

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.

Doporučená 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-1

Zařazení předmětu ve studijních plánech

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

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

Typ (způsob) výuky

 

Přednáška

39 hod., nepovinná

Vyučující / Lektor

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

Osnova

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

Cvičení na počítači

6 hod., nepovinná

Vyučující / Lektor

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

Osnova

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

Projekt

7 hod., nepovinná

Vyučující / Lektor

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