|
ECTS:
|
6
|
Lecturers in charge:
|
Prof. dr. sc.
Bruno Blašković
|
English level:
1,1,1
|
All teaching activities in the course will be held on English. This level includes courses with multiple groups (i.e., all teaching will be held strictly in Croatian for Croatian groups, and strictly in English for English groups).
|
Description:
|
Real-Time system as a set of elementary communicating processes. Formal methods: algebraic, net and logic models with application to verification and specification. Real-Time UML, SDL and synchronous languages. Language pair system analysis, reachability algorithms, theorem proving. Synthesis as a composition of coordinating processes. Real-Time scheduling and allocation. Tools and languages for analysis. Examples: concurrent reactive systems, protocols, parallel algorithms, model extraction.
|
Literature:
|
- 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 semester
|
course for
Graduation study
|
|
