Modeling with Uppaal: The Production Cell Assignment
The purpose of this lab is to give the students an introduction to formal methods and model checking by modeling and verifying an industrial production cell application using the Uppaal tool. During this lab, the students will first model a production cell by the means of timed automata communicating over a set of channels. Each of these automata represents a component in the production cell (feed belt, robot arm...). Then, the students will check the model against many properties. For example, verify that the system is deadlock free.
Getting started with Uppaal
Unless you already used Uppaal earlier, you probably want to get familiar with the tool first: Uppaal tutorial.
Please do not submit any report for the tutorial. The tutorial is there to help you, it is not part of the assignment.
You might also check out the home page of Uppaal for further documentation and help.
In order to start Uppaal, use the following script: Enter this directory /stud/docs/kurs/realtid/production_cell and start the script uppaal2k.
- The assignment is available here: Production Cell
- The xml model you have to start from is availabale here: Production Cell Model
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:
- Answers and discussions on the properties that must be verified.
You are allowed to work alone or in pairs.
What you have to submit is the following:
- A report (with your names and personnal numbers) where you provide answers and discussions on the properties that must be verified.
- The xml file of your model.
How to submit:
- Send me copies of your files to this adress Noomene.BenHenda@it.uu.se
Grading and Deadline
You will be receiving grading automatically via the course manager system. Please check that you can login to the system and that your name is there. Otherwise, tell me about it as soon as possible. Here is the link Course Manager.
The first deadline is: 2006/12/15