for students of computer studies (2 year, master).
kod kursu: INEA12103L
Students model, simulate and verify communication and transportation systems, using Petri Nets, temporal logic and timed automata.
The laboratories on Petri Nets last the first 5 periods; the laboratories on Temporal Logic and Timed Automata last the last 5 periods of the Information Systems Analysis.
The exercises on Temporal Logic and Timed Automata may be done by students in 2-persons teams.
- part (period 1): Intruduction to Petri Nets
- Students build and simulate simple ordinary Petri Nets.
- Deadline for the report: period 2
- part (periods 2 – 3): Ordinary Petri Nets
- Students develop Petri Nets models.
- Deadline for the report: period 4
- part (periods 4 – 5): Timed Petri Nets
- Students develop Timed Petri Nets models.
- Deadline for the report: period 5
Temporal Logic and Timed Automata
- part (period 11): UPPAAL Timed Automata
- Students learn to use the UPPAAL tool and model and simulate simple timed automata.
- Deadline for the report: period 12
- part (periods 12 – 13): System Model Verification in UPPAAL
- Students create and interprete CTL formulas, and model and verify systems.
- Deadline fot the report: period 14
- part (periods 14 – 15): System Model Verification in NuSMV
- Students learn how to use the NuSMV tool, they create and interprete LTL, CTL and RTCTL formulas, and model and verify systems.
- Deadline for the report: February, 2.
Reports must be printed or written on paper. Please, give your name, surname and student ID number in the upper left corner of the report’s cover. Do not staple the sheets, use a paper clip instead.
A report must contain results of all exercises given in a laboratory instruction.
Do not add any theory or other stuff, that is not asked for in the laboratory instraction.
Correction of a report, that was low graded, is not mandatory. Yet, it is possible within one week.
Students will get grades for every final version of their reports. These are the partial grades.
The mean value of 3 partial grades for reports on the Petri Nets is the grade for the subject. The mean value of 3 partial grades for reports on the Temporal Logic and Timed Automata is the grade for the subject. Alltogether with a grade for Queing Models, these 3 grades make the final grade.