Information Systems Analysis (laboratories)

for students of computer studies (2 year, master).
kod kursu: INEA12103L

Laboratories of Information Systems Analysis is: modeling, simulation and verification of communication and transportation systems, using Petri Nets, temporal logic and timed automata.

The course is divided into 3 5-periods parts:

  1. Petri Nets.
  2. Queueing models.
  3. Temporal Logic and Timed Automata.

The exercises of the 1st and 3rd part are to be done by students in 2-persons teams.


Petri Nets

  • period 1 (exercises): Intruduction to Petri Nets – construction and simulation of simple Petri Nets. Report deadline: period 2.
  • periods 2–3 (exercises): Ordinary Petri Nets – construction and simulation of complex Petri Nets. Report deadline: period 4.
  • period 4 (exercises): Timed Petri Nets – construction and simulation of Timed Petri Nets. Report deadline: period 5.
  • period 5 (exercises): Other features of Petri Nets – construction and reconstruction of Petri Nets. Report deadline (delivered by e-mail or during office hours): period 7.

Temporal Logic and Timed Automata

  • period 11 (exercises): UPPAAL Timed Automata – construction, simulation and verification of simple UPPAAL automata. Report deadline: period 12.
  • period 12–13 (exercises): System Model Verification in UPPAAL – construction, simulation and verification of complex UPPAAL automata. Report deadline: period 14.
  • period 14–15 (exercises): System Model Verification in NuSMV – construction and verification of complex NuSMV automata. Report deadline: January, 24.

How to install and use the NuSMV on Linux (Ubuntu)


Useful sites


Reports must be printed or written on paper. Please, give your name, surname and student ID number in the upper left corner of the 1st page. Do not staple the sheets, use a paper clip instead.

A report must contain results of all exercises given in a laboratory instruction.

Correction of a report, that was low graded, is not mandatory. Yet, it is possible within one week.


Partial and final grades

Students will get grades for every final version of their reports. These are the partial grades.

The final grade for the 1st part is the mean value of all reports thereof.

The final grade for the 3st part is the mean value of all reports thereof.

The final grade is the mean value of final grades from all the 3 parts.

Comments are closed.