Název:

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

Zkratka:SVSe
Ak.rok:2012/2013
Semestr:letní
Studijní plán:
ProgramOborRočníkPovinnost
IT-MGR-2MBI-volitelný
IT-MGR-2MBS-povinně volitelný - skupina C
IT-MGR-2MGM-volitelný
IT-MGR-2MIN-volitelný
IT-MGR-2MIS-povinně volitelný - skupina F
IT-MGR-2MMI-povinně volitelný - skupina M
IT-MGR-2MMM-volitelný
IT-MGR-2MPV-volitelný
IT-MGR-2MSK2.povinně volitelný - skupina C
IT-MGR-2EITE2.volitelný
Vyučovací jazyk:angličtina
Aktuální informace:This course is instructed in English, and it is prepared for incoming LLP/Erasmus students too.
Kredity:5 kreditů
Ukončení:zkouška (kombinovaná)
Výuka:
hod./sempřednáškasem./cvičenílab. cvičenípoč. cvičeníjiná
Rozsah:390067
 zkouškatestycvičenílaboratořeostatní
Body:60150025
Garant:Švéda Miroslav, prof. Ing., CSc., UIFS
Přednášející:Ryšavý Ondřej, Ing., Ph.D., UIFS
Švéda Miroslav, prof. Ing., CSc., UIFS
Cvičící:Ryšavý Ondřej, Ing., Ph.D., UIFS
Fakulta:Fakulta informačních technologií VUT v Brně
Pracoviště:Ústav informačních systémů FIT VUT v Brně
Nahrazuje:
Komunikace v počítačových aplikacích (KPA), UIFS
 
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ů.
Anotace:
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.
Požadované prerekvizitní znalosti a dovednosti:
Výroková logika. Základy predikátové logiky 1. řádu. Základní pojmy komunikačních protokolů.
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.
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
  4. Základy temporální logiky
  5. Časové modely a temporální logiky
  6. Temporální logika a reálný čas
  7. Formální specifikace vestavěných systémů
  8. Dokazovací systémy
  9. Kontrola modelem
  10. Verifikace systémů pracujících v reálném čase
  11. Formální specifikace abstraktních datových struktur a objektů, algebraické specifikace
  12. Použití systémů teorie typů pro specifikaci a ověření programů
Osnova numerických cvičení:
  1. 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 laboratorních cvičení:
  1. Správa vestavěné aplikace z intranetu
Osnova počítačových cvičení:
  1. Úvodní sezenámení se systémem Coq, specifikace jednoduchých vlastností
  2. Základní techniky specifikace programů
  3. Ověřování správnosti jednoduchého algoritmu
Osnova ostatní - projekty, práce:
  1. Formální specifikace a verifikace vlastností vestavěného systému
Literatura referenční:
  1. Schneider, K.: Verification of Reactive Systems, Springer-Verlag, 2004, ISBN 3-540-00296-0 
  2. 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
  3. Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000, ISBN 0-262-03270-8
  4. de Bakker, J.W. et all. (Editors): Real-Time: Theory in Practice, Springer-Verlag, LNCS 600, 1992, ISBN 3-540-55564-1
  5. Gabbay, D.M., Ohlbach, H.J. (Editors): Temporal Logic, Springer-Verlag, LNCS 827, 1994, ISBN 3-540-58241-X
  6. Monin, J.F., Hinchey, M.G.:Understanding Formal Methods, Springer-Verlang, 2003.
  7. Peled, D.A.:Software Reliability Methods, Text in Computer Science, Springer, 2001.
  8. Tennent, R.D.:Specifying Software: A Hand-On Introduction, Cambridge University Press, 2002.
  9. Bertot, Y., Casteran, P.:Interactive Theorem Proving and Program Development, Springer-Verlang, 2004.
Literatura studijní:
  1. 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
  2. Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000, ISBN 0-262-03270-8
  3. de Bakker, J.W. et all. (Editors): Real-Time: Theory in Practice, Springer-Verlag, LNCS 600, 1992, ISBN 3-540-55564-1
  4. Peregrin, J.: Logika a logiky, Academia, 2004, ISBN 80-200-1187-0
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. 
Průběžná kontrola studia:
Protokol o laboratorní úloze, půlsemestrální test a vypracování  projektu v předepsaném termínu.
Podmínky zápočtu:
Zápočet není ustanoven.