Název:

Specifikace vestavěných systémů

Zkratka:SVD
Ak.rok:2012/2013
Semestr:zimní
Studijní plán:
ProgramOborRočníkPovinnost
VTI-DR-4DVI4-volitelný
Vyučovací jazyk:čeština
Ukončení:zkouška (ústní)
Výuka:
hod./sempřednáškasem./cvičenílab. cvičenípoč. cvičeníjiná
Rozsah:390000
 zkouškatestycvičenílaboratořeostatní
Body:00000
Garant:Švéda Miroslav, prof. Ing., CSc., UIFS
Fakulta:Fakulta informačních technologií VUT v Brně
Pracoviště:Ústav informačních systémů FIT VUT v Brně
 
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.
Anotace:
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.
Požadované prerekvizitní znalosti a dovednosti:
Základní přednášky matematiky na technických universitách
Získané dovednosti, znalosti a kompetence:
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ů.
Osnova přednášek:
  1. Principy návrhu vestavěných distribuovaných systémů
  2. Modely reaktivních systémů a systémů pracujících v reálném čase
  3. Spravedlivost, živost, bezpečnost, realizovatelnost; živost reálného času, odezva v konečném čase
  4. Základy temporální logiky: syntaxe, sémantika, axiomatika
  5. Časové modely a temporální logiky
  6. LTL
  7. CTL
  8. Temporální logika a reálný čas
  9. Formální specifikace vestavěných systémů
  10. Dokazovací systémy
  11. Kontrola modelem
  12. Verifikace systémů pracujících v reálném čase
  13. Případové studie
Osnova ostatní - projekty, práce:
  1. 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.
Literatura referenční:
  1. Schneider K.: Verification of Reactive Systems -- Formal Methods and Algorithms. Springer-Verlag, 2004.
  2. Huth M.R.A., Ryan M.D.: Logic in Computer Science -- Modelling and Reasoning about Systems. Cambridge University Press, 2000.
  3. de Bakker J.W. et all. (Editors): Real-Time: Theory in Practice. Springer-Verlag, LNCS 600, 1992.
  4. Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. Springer-Verlag, LNCS 827, 1994.
Literatura studijní:
  1. Bowen J.P., Hinchey M.G.: High-Integrity System Specification and Design. Springer-Verlag, 1999.
  2. Huth M.R.A., Ryan M.D.: Logic in Computer Science -- Modelling and Reasoning about Systems. Cambridge University Press, 2000.
  3. Schneider K.: Verification of Reactive Systems -- Formal Methods and Algorithms. Springer-Verlag, 2004.
  4. de Bakker J.W. et all. (Editors): Real-Time: Theory in Practice. Springer-Verlag, LNCS 600, 1992.
  5. Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. Springer-Verlag, LNCS 827, 1994.
  6. Johnsson B., Parrow J.: Formal Techniques in Real-Time and Fault Tolerant Systems. Springer-Verlag, LNCS 1135, 1996.
Kontrolovaná výuka:
Zpracovaní a obhájení eseje.