Detail předmětu

Specifikace vestavěných systémů

FIT-SVDAk. rok: 2017/2018

Principy návrhu vestavěných distribuovaných systémů vycházející z formálních specifikací chování. Reaktivní systémy a systémy pracující v reálném čase: úroveň abstrakce, podobnost a rozdíly. Modely reaktivních systémů a systémů pracujících v reálném čase: stavové posloupnosti a stromy, časované stavové posloupnosti, konečné automaty; Kripkeho struktury. Základní logické vlastnosti: spravedlivost, živost, bezpečnost, realizovatelnost; živost reálného času, odezva v konečném čase. Modální logiky a temporální logiky: kripkovské sémantiky. Základy temporální logiky: syntaxe, sémantika, axiomatika. Časové modely a temporální logiky: uspořádanost, budoucnost x minulost, diskrétní x hustý x spojitý, počátek času, konec času. LTL. CTL. Temporální logika a reálný čas: pozorovací posloupnosti; přístup Alura a Henzingera; přístup Koymanse a Vytopila a de Roevera; přístup Pnueliho a de Roevera. Formální specifikace vestavěných systémů. Dokazovací systémy. Kontrola modelem. Verifikace systémů pracujících v reálném čase. Případové studie.

Okruhy otázek k SDZ:

  1. Teorie systémů: transformační, reaktivní a RT
  2. Model chování diskrétního systému stavovou posloupností - vlastnosti: bezpečnost, živost, spravedlivost
  3. Významy a reprezentace pojmu "čas"
  4. Model chování RT systému časovanou stavovou posloupností - vlastnosti: bezpečnost, živost, spravedlivost; logické vlastnosti chování v reálném čase
  5. Čas v distribuovaných systémech: a) Lamportův model, logické hodiny, fyzické hodiny; b) model Goswamiho a Josepha
  6. Modální a temporální logika, Kripkeho sémantika
  7. Tradiční propoziční temporální logika, axiomatická báze, její nerozpornost a úplnost, interpretace
  8. Dokazování a model checking
  9. Časové modely a propoziční temporální logiky
  10. RT rozšíření temporálních logik

Jazyk výuky

čeština

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í principům formálních specifikací 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ů.

Prerekvizity

Základní přednášky matematiky na technických universitách

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

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, odezva v konečném čase
    • Základy temporální logiky: syntaxe, sémantika, axiomatika
    • Časové modely a temporální logiky
    • LTL
    • CTL
    • 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
    • Případové studie

    Osnova ostatní - projekty, práce:
    • Prostudování a zpracování formou eseje vybraného vědeckého článku z oblasti aplikace temporálních logik v problematice řešené v disertační práci studenta.

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 metodách verifikace.

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

Zpracovaní a obhájení eseje.

Základní literatura

Schneider K.: Verification of Reactive Systems -- Formal Methods and Algorithms. Springer-Verlag, 2004. Huth M.R.A., Ryan M.D.: Logic in Computer Science -- Modelling and Reasoning about Systems. Cambridge University Press, 2000. de Bakker J.W. et all. (Editors): Real-Time: Theory in Practice. Springer-Verlag, LNCS 600, 1992. Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. Springer-Verlag, LNCS 827, 1994.

Doporučená literatura

Bowen J.P., Hinchey M.G.: High-Integrity System Specification and Design. Springer-Verlag, 1999. Huth M.R.A., Ryan M.D.: Logic in Computer Science -- Modelling and Reasoning about Systems. Cambridge University Press, 2000. Schneider K.: Verification of Reactive Systems -- Formal Methods and Algorithms. Springer-Verlag, 2004. de Bakker J.W. et all. (Editors): Real-Time: Theory in Practice. Springer-Verlag, LNCS 600, 1992. Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. Springer-Verlag, LNCS 827, 1994. Johnsson B., Parrow J.: Formal Techniques in Real-Time and Fault Tolerant Systems. Springer-Verlag, LNCS 1135, 1996.

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

  • Program VTI-DR-4 doktorský

    obor DVI4 , 0 ročník, zimní semestr, volitelný