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.

Agenda

Petri Nets

  1. part (period 1): Intruduction to Petri Nets
    • Construction and simulation of simple Petri Nets.
    • Deadline for the report: period 2.
  2. part (periods 2 – 3): Ordinary Petri Nets
    • Construction and simulation of complex Petri Nets.
    • Deadline for the report: period 4.
  3. part (period 4): Timed Petri Nets
    • Construction and simulation of Timed Petri Nets.
    • Deadline for the report: period 5.
  4. part (period 5): Other features of Petri Nets
    • Construction and reconstruction of different Petri Nets.
    • Deadline for the report (to be delivered by e-mail or during office hours): period 7.

Temporal Logic and Timed Automata

  1. part (period 11): UPPAAL Timed Automata
    • Construction, simulation and verification of simple automata.
    • Deadline for the report: period 12.
  2. part (periods 12 – 13): System Model Verification in UPPAAL
    • Construction, simulation and verification of complex automata.
    • Deadline fot the report: period 14.
  3. part (periods 14 – 15): System Model Verification in NuSMV
    • Construction and verification of complex automata.
    • Deadline for the report: January, 24.

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

Tools

Useful sites

Reports

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.

Grades

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.