Fakulta informačních technologií VUT v Brně

Detail předmětu

Specifikace vestavěných systémů (v angličtině)

SVSe Ak. rok 2011/2012 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

anglicky

Zakončení

zkouška (kombinovaná)

Rozsah

39 hod. přednášky, 6 hod. cvičení, 7 hod. projekty

Bodové hodnocení

60 zkouška, 15 půlsemestrální test, 25 projekty

Zajišťuje ústav

Přednášející

Cvičící

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

Dovednosti, znalosti a kompetence obecné

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
  • Peregrin, J.: Logika a logiky, Academia, 2004, ISBN 80-200-1187-0

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 numerických cvičení

  • Představení systému Coq - stručné vysvětlení použitého formalismu nástroje, představení příkazového jazyka nástroje, demonstrace základních konkstrukcí jazyka a ukázka specifikace a ověření vlastností jednoduchého algoritmu

Osnova ostatní - projekty, práce

  • Formální specifikace a verifikace vlastností vestavěného systému

Průběžná kontrola studia

Protokol o laboratorní úloze, půlsemestrální test a vypracování  projektu v předepsaném termínu.

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. 

Podmínky zápočtu

Zápočet není ustanoven.

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

  • Program IT-MGR-2, obor MBI, MGM, MGM., MIN, MIN., MMM, MPS, MPV, libovolný ročník, volitelný
  • Program IT-MGR-2, obor MBS, libovolný ročník, povinně volitelný skupina C
  • Program IT-MGR-2, obor MIS, libovolný ročník, povinně volitelný skupina F
  • Program IT-MGR-2, obor MIS., 1. ročník, volitelný
  • Program IT-MGR-2, obor MMI, libovolný ročník, povinně volitelný skupina M
  • Program IT-MGR-2, obor MSK, 2. ročník, povinně volitelný skupina C
Nahoru