Název:

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

Zkratka:SVS
Ak.rok:ukončen 2006/2007
Semestr:letní
Studijní plán:
ProgramObor/
specializace
RočníkPovinnost
IT-MGR-2MGM.-volitelný
IT-MGR-2MIN.-volitelný
IT-MGR-2MIS.1.volitelný
IT-MGR-2MPS-volitelný
Vyučovací jazyk:čeština, angličtina
Informace pro zapsané:http://www.fit.vutbr.cz/study/courses/SVS/private/
Kredity:5 kreditů
Ukončení:zkouška (písemná)
Výuka:
hod./sempřednáškasem./cvič.lab. cvič.poč. cvič.jiná
Rozsah:390067
 zkouškatestycvičenílaboratořeostatní
Body:60150025
Garant:Švéda Miroslav, prof. Ing., CSc. (UIFS)
Přednášející:Š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. Protokoly typu Fieldbus. Internet a vestavěné systémy.
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
  • Hybridní systémy
  • Protokoly typu Fieldbus
  • Internet a vestavěné systémy
Osnova laboratorních cvičení:
 
  • Správa vestavěné aplikace z intranetu
Osnova počítačových cvičení:
 
  • Spin, techniky kontroly modelem
  • PVS, techniky dokazování
Osnova ostatní - projekty, práce:
 
  • Formální specifikace vestavěného systému
  • 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
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í 2 projektů v předepsaných termínech.
Podmínky zápočtu:
  Zápočet není ustanoven.
 

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

DNSSEC [dnssec]