Detail předmětu
Specifikace vestavěných systémů
SVD Ak. rok 2006/2007 zimní semestr
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.
Garant předmětu
Jazyk výuky
Zakončení
Rozsah
- 39 hod. přednášky
Zajišťuje ústav
Získané dovednosti, znalosti a kompetence z 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ů.
Cíle předmětu
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.
Požadované prerekvizitní znalosti a dovednosti
Základní přednášky matematiky na technických universitách
Literatura studijní
- 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.
Literatura referenční
- 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.
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
Průběžná kontrola studia
Hodnocení studia je založeno na bodovacím systému. Pro úspěšné absolvování předmětu je nutno dosáhnout 50 bodů.
Kontrolovaná výuka
Zpracovaní a obhájení eseje.