for students of computer studies (2 year, master)
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:
- Petri Nets.
- Queueing models (with another teacher).
- 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).
You may have a maximum of 2 unexcused absences from classes. Absence from more than half of the classes may result in failing the course.
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.
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 classes 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.
Students learn about grades during classes where they receive them. If necessary, this information can be sent via email.
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.