Název:

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

Zkratka:SVSe
Ak.rok:2011/2012
Semestr:letní
Studijní plán:
ProgramOborRočníkPovinnost
IT-BC-1HBCH-volitelný
IT-MGR-1HMGH-volitelný
IT-MGR-2MBI-volitelný
IT-MGR-2MBS-povinně volitelný - skupina C
IT-MGR-2MGM-volitelný
IT-MGR-2MGM.-volitelný
IT-MGR-2MIN-volitelný
IT-MGR-2MIN.-volitelný
IT-MGR-2MIS-povinně volitelný - skupina F
IT-MGR-2MIS.1.volitelný
IT-MGR-2MMI-povinně volitelný - skupina M
IT-MGR-2MMM-volitelný
IT-MGR-2MPS-volitelný
IT-MGR-2MPV-volitelný
IT-MGR-2MSK2.povinně volitelný - skupina C
IT-MGR-2EITE2.volitelný
Vyučovací jazyk:angličtina
Kredity:5 kreditů
Ukončení:zkouška (kombinovaná)
Výuka:
hod./sempřednáškasem./cvičenílab. cvičenípoč. cvičeníjiná
Rozsah:396007
 zkouškatestycvičenílaboratořeostatní
Body:60150025
Garant:Švéda Miroslav, prof. Ing., CSc., UIFS
Přednášející:Ryšavý Ondřej, doc. Ing., Ph.D., UIFS
Švéda Miroslav, prof. Ing., CSc., UIFS
Cvičící:Ryšavý Ondřej, doc. 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:
 
  • 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 laboratorních cvičení:
 
  • Správa vestavěné aplikace z intranetu
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
Osnova ostatní - projekty, práce:
 
  • Formální specifikace a verifikace vlastností vestavěného systému
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.
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
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.