Assignment 2
Modeling with Uppaal: The Production Cell Assignment
Second assignment pdf
ps is available. It's deadline is on the 16 January 2006 and is to be solved individually or in pairs.
Getting started with Uppaal
Unless you already used Uppaal earlier, you probably want to get familiar with the tool first.
Uppaal tutorial pdf ps.
Please do not submit any report for the tutorial. The tutorial is there to help you, it is not part of the assignment.
To start Uppaal please use the following script:
/home/thereseb/LabbHandledning/Datorsystem2HT05/uppaal-3.4.11/uppaal
Erratum for the assignment
The assignment was picked from year 2002. Some of the text does not apply to this instance of the course.
- Page 6: The lab instructions describe a complex procedure involving a console-based tool, verifyta, to check for deadlocks (the first bullet on what you need to verify). This can now be done easily from Uppaal using the query "A[] not deadlock".
- Page 8: Disregard the general guidelines for your report. What you must do is the following:
- The report must include a print-out of the robot FSM.
- Answers and discussions on the properties that must be verified.
- An e-mail with the Uppaal model of the system and the name/s of the constructor/s sent to thereseb@it.uu.se.