Detail předmětu
Specifikace vestavěných systémů (v angličtině)
SVSe Ak. rok 2013/2014 letní semestr 5 kreditů
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.
Garant předmětu
Jazyk výuky
Zakončení
Rozsah
- 39 hod. přednášky
- 6 hod. pc laboratoře
- 7 hod. projekty
Zajišťuje ústav
Získané dovednosti, znalosti a kompetence z 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.
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 architekturách vestavěných distribuovaných systémů.
Požadované prerekvizitní znalosti a dovednosti
Výroková logika. Základy predikátové logiky 1. řádu. Základní pojmy komunikačních protokolů.
Literatura studijní
- 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
Literatura referenční
- 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.
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 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
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ů.
Zápočet není ustanoven.
Metody vyučování
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ě.
Kontrolovaná výuka
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.
Zařazení předmětu ve studijních plánech