|
ECTS:
|
6
|
Nositelji:
|
Prof. dr. sc.
Bruno Blašković
|
Engleski jezik:
1,1,1
|
Svi elementi nastave na predmetu provode se na engleskom jeziku. Ova razina uključuje i predmete s više nastavnih grupa (u hrvatskoj grupi nastava je isključivo na hrvatskom jeziku, a u engleskoj grupi isključivo na engleskom jeziku).
|
Opis predmeta:
|
Stvarnovremenski sustav kao skup elementarnih komunicirajućih procesa. Formalne metode opisa: algebarski, mrežni i logički modeli sa primjenom na specifikaciju i verifikaciju. Reaktivni UML, SDL i sinkroni jezici. Analiza sa jezičnim parovima, algoritmi dostupnosti, dokazivanje teorema. Sinteza kao kompozicija koordinirajućih procesa. Raspodjela i alokacija procesa. Programski alati i jezici za analizu. Primjeri: protokoli, paralelni algoritmi, konkurentni reaktivni sustavi, model ekstrakcija.
|
Literatura:
|
- K. Schneider: Verification of Reactive Systems, Springer 2004.
- G. Holzmann: The SPIN model checker, Addison-Wesley, 2003.
- M. Bernardo, F. Corradini (ur.): Formal Methods for the Design of Real-Time Systems, LNCS 3185, Springer, 2004.
|
|
Zimski semestar
|
predmet za
Poslijediplomski studij
|
|
