Detail předmětu

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

FIT-SVSeAk. rok: 2014/2015

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ů

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

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

    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 algoritmu

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

    Osnova ostatní - projekty, práce:
    • Formální specifikace a verifikace vlastností vestavěného systému

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 MMI , 0 ročník, letní semestr, povinně volitelný
    obor MBI , 0 ročník, letní semestr, volitelný
    obor MSK , 2 ročník, letní semestr, povinně volitelný
    obor MMM , 0 ročník, letní semestr, volitelný
    obor MBS , 0 ročník, letní semestr, povinně volitelný
    obor MPV , 0 ročník, letní semestr, volitelný
    obor MIS , 0 ročník, letní semestr, povinně volitelný
    obor MIN , 0 ročník, letní semestr, volitelný
    obor MGM , 0 ročník, letní semestr, volitelný