Název:

Formální specifikace systémů založených na počítačích

Zkratka:SSD
Ak.rok:2012/2013
Semestr:letní
Studijní plán:
ProgramOborRočníkPovinnost
VTI-DR-4DVI4-volitelný
Vyučovací jazyk:čeština
Ukončení:zkouška (ústní)
Výuka:
hod./sempřednáškasem./cvičenílab. cvičenípoč. cvičení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ě
Prerekvizity: 
Specifikace vestavěných systémů (SVSe), UIFS
 
Cíle předmětu:
Být informován o principech formálních specifikací a jejich uplatnění při návrhu systémů založených na počítačích a jejich komponent.
Anotace:
Cílem tohoto předmětu je nabídnout přehled typických formálních nástrojů využitelných pro specifikace chování systémů založených na počítačích a komponent těchto systémů. Po absolvování přehledu každý student zvolí vhodný nástroj aplikovatelný v rámci tématu jeho disertace a prostuduje jej podrobněji. Přehled pokryje podoblasti s následujícími příklady nástrojů a metod: Konečné automaty, omega-automaty, časované automaty. Principy algeber procesů, BPA. Příklady algeber procesů: CSP, CCS. Algebry časovaných procesů, TCSP. Přehled temporálních logik. Temporální specifikace vlastností typu: dosažitelnost, bezpečnost, živost, spravedlivost, odezva v omezeném čase, ... . Příklady temporálních logik reálného času. Vzájemné souvislosti dokazování a kontroly modelu. Algebry procesů a temporální logiky. Teorie stop a ostatní teorie. Vzájemné souvislosti. Případové studie.
Požadované prerekvizitní znalosti a dovednosti:
Základní přednášky matematiky na technických universitách
Získané dovednosti, znalosti a kompetence:
Informovanost o principech formálních specifikací a o současném stavu jejich uplatnění při návrhu systémů založených na počítačích.
Osnova přednášek:
  1. Systémy založené na počítačích a jejich specifikace
  2. Konečné automaty, omega-automaty, časované automaty
  3. Principy algeber procesů, BPA; příklady algeber procesů, CSP, CCS 
  4. Algebry procesů reálného času, TCSP
  5. Přehled temporálních logik
  6. Temporální specifikace vlastností typu: dosažitelnost, bezpečnost, živost, spravedlivost, odezva v omezeném čase, ... 
  7. Příklady temporálních logik reálného času; TLA jako logika reálného času 
  8. Dokazování
  9. Kontrola modelu
  10. Algebry procesů a temporální logiky
  11. Teorie stop
  12. Vzájemné souvislosti
  13. Případové studie
Osnova ostatní - projekty, práce:
  1. Prostudování a zpracování formou eseje vybraného formálního aparátu automatů, algeber procesů, temporálních logik resp. teorie stop aplikovaného na problematiku řešenou v disertační práci studenta.
Literatura referenční:
  1. Berard B. et al.: Systems and Software Verification. Springer-Verlag, 2001.
  2. Clarke E.M., Jr., Grumberg O., Peled D.A.: Model Checking. MIT Press, 2000.
  3. Schneider K.: Verification of Reactive Systems. Springer-Verlag, 2004.
  4. de Bakker J.W., de Roever W.-P., Rozenberg G. (Editors): Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. Springer-Verlag, LNCS 354, 1989.
  5. Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. Springer-Verlag, LNCS 827, 1994.
  6. Huth M.R.A., Ryan M.D.: Logic in Computer Science -- Modelling and Reasoning about Systems. Cambridge University Press, 2002.
Literatura studijní:
  1. Kreowski H.-J., Montanari U., Orejas F., Rozenberg G., Taentzer G.: Formal Methods in Software and Systems Modeling. Springer, LNCS 3393, 2005.
  2. Berard B. et al.: Systems and Software Verification. Springer-Verlag, 2001.
  3. Clarke, E.M., Jr., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
  4. Schneider K.: Verification of Reactive Systems. Springer-Verlag, 2004.
  5. Abramsky S., Gabbay D.M., Maibaum T.S.E. (Editors): Handbook of Logic in Computer Science. Volumes 1, 2, 3, 4, 5. Oxford Science Publications, 2000.
  6. de Bakker J.W., de Roever W.-P., Rozenberg G. (Editors): Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. Springer-Verlag, LNCS 354, 1989.
  7. Gabbay D.M., Ohlbach H.J. (Editors): Temporal Logic. Springer-Verlag, LNCS 827, 1994.
  8. Huth M.R.A., Ryan M.D.: Logic in Computer Science -- Modelling and Reasoning about Systems. Cambridge University Press, 2002.
Kontrolovaná výuka:
Zpracovaní a obhájení eseje.