Název:

Specifikace vestavěných systémů

Zkratka:SVD
Ak.rok:2013/2014
Semestr:zimní
Studijní plán:
ProgramObor/
specializace
RočníkPovinnost
VTI-DR-4DVI4-volitelný
Vyučovací jazyk:čeština
Ukončení:zkouška (ústní)
Výuka:
hod./sempřednáškasem./cvič.lab. cvič.poč. cvič.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.

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
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:
 
  • 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.
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.
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.
Kontrolovaná výuka:
  Zpracovaní a obhájení eseje.
 

Vaše IPv4 adresa: 18.206.168.65
Přepnout na https

DNSSEC [dnssec]