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

Before the course starts, please read this whole site.

Organisation of the laboratories

The goal of this course is to model, simulate and verify communication and transportation systems, using Petri Nets, quening networks, temporal logic and timed automata.

The course is divided into 3 5-periods parts:

1. Petri Nets.
2. Queueing models (with another teacher).
3. Temporal Logic and Timed Automata*.

* the word „automata” is a plural form of the word „automaton”.

The following applies to the 1st and the 3rd parts of the course only. The 2nd part is taught, organised and graded by dr Tomasz Babczyński.

All exercises are done by students individually (not in teams).

The course in the winter semester 2021/2022 takes place stationary (in the campus).

This site contains the following: agenda of the laboratories (with exercises and deadlines to do them), tools to use, requirements for content and format of reports from the laboratories, and grading rules.

For sanitary reasons, people in the laboratory must keep their mouth and nose covered and keep a safe distance from each other. A person with a runny nose or cough or a high temperature should stay at home.

Agenda

Petri Nets

Introduction to laboratories 1–3: in English, po polsku
Introduction to laboratories 4: in English, po polsku
Introduction to laboratories 5: in English, po polsku

• laboratories 1 (exercises): Construction and behavioral analysis of Petri nets. Deadline for the report: laboratories 2.
• laboratories 2 (exercises): Construction of Petri nets with inhibitor arcs (part 1). Deadline for the report: laboratories 3.
• laboratories 3 (exercises): Construction of Petri nets with inhibitor arcs (part 2). Deadline for the report: laboratories 4.
• laboratories 4 (exercises): Construction of Petri nets with timed arcs. Deadline for the report: laboratories 5.
• laboratories 5 (exercises): Construction of generalised stochastic Petri nets. Deadline for the report: laboratories 6.

See Welcome to the Petri Nets World for more information on Petri Nets.

Temporal Logic and Timed Automata

Introduction to laboratories 11–13: in English, po polsku
Introduction to laboratories 14–15: in English, po polsku

• laboratories 11 (exercises): Construction of simple UPPAAL automata. Deadline for the report: laboratories 12.
• laboratories 12 (exercises): Construction and verification of
  synchronized timed UPPAAL automata (part 1). Deadline for the report: laboratories 13.
• laboratories 13 (exercises):Construction and verification of
  synchronized timed UPPAAL automata (part 2). Deadline for the report: laboratories 14.
• laboratories 14 (exercises): Construction and verification of synchronized NuSMV automata. Deadline for the report: laboratories 15.
• laboratories 15 (exercises): Construction and verification of NuSMV automata for analysis of a program.Deadline for the report: in a week, thourgh the e-mail.

Tools

Download and use some of the following tools to do exercises. They are free, they run on Java and they need no installation.

• TAPAAL – for normal and timed Petri nets
• Pipe – for normal and generalised stochastic Petri nets
• Oris – for generalised stochastic Petri nets
• UPPAAL – for timed automata with CTL logic
• NuSMV – for automata with LTL, CTL and TCTL logic

See how to configure and use NuSMV on Ubuntu Linux.

Reports

Every laboratory meating concludes by a report with results from its exercises.

The report must be a pdf file with a description of what has been done, especially: pictures with Petri nets or UPPAAL automata templates, and code for UPPAAL or NuSMV automata with its explenation. No theory or conclusions is needed.

The report from the laboratory n should be e-mailed untill the laboratory n+1 starts, or within one week in case of the last laboratory. Please, give your name, surname and student ID number in the upper left corner of the 1st page. Also put the acronim ISA in the subject of the e-mail, together with your surname and the number of the laboratories.

Together with the report, sent all the files you have made to do the exercises.

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

Grades

Students get grades for every final verion of their report. These are partial grades. A partial grade depands on points for exercises (grade = pts/2). You can get up to 10 pts for every laboratory.

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

The final grade for the 2st part is defined and given by its teacher.

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

The final grade is the mean value of final grades from all the 3 parts, or 2.0 if at least one of the parts ends with such a partial grade.