Modelling in Times
The assignment should give the student a chance to use a tool for modeling and formal analysis of real-time systems.
The assignment consists of three parts and should be solved individually or in groups of two. The assignment must be handed in no later than December 22, 09:00.
The Times 1.2beta is installed on the UNIX machines at DoCS at /it/kurs/realtid/realtid.OLD/Timestool/Timestool. You can create a link or an alias for it if you like.
In section WorkingHome below you may find instruction on how to download and run Times at home.
A Coffee Machine
The main purpose of this part is to familiarize yourself with the Times tool. You will use the editor, the simulator and you will verify some properties.
As you all know, a large amount of coffee is necessary to produce good results, (especially in academia). This first assignment lets you construct a system which maximizes the number of (academic) publications produced.
You are asked to design the control of a (coffee) Machine (the control program) which will serve a coffee for the Person (eg. a PhD student). As you can see above the Person repeatedly (tries to) insert a coin, (tries to) extract coffee after which (s)he will make a publication. Between each action the Person requires a suitable time-delay before being ready to participate in the next one.
After receiving a coin the Machine should take some time for brewing the coffee. The Machine should time-out if the brewed coffee has not been taken before a certain upper time-limit.
As a requirement we want the overall behaviour to ensure that the indicated Observer (eg. some demanding professor or funding institute) experiences a constant flow of publications from the Person. In particular we want the Observer to complain if at any time more than 8 time-units elapse between two consecutive publications. Model the Machine, the Person, and the Observer in Times and analyze the behaviour of the system. You must use the Verifier to determine this, for example with a query A not Observer.complain if we assume that the Observer automaton has a location named complain. You will probably want to
use some other queries as well.
After creating the Machine, Person and Observer automata, try to determine the maximum brewing time allowed by the Machine in order that the above requirement is met. Also here the Verifier will help you.
What to report:
- The models of the Observer, Machine and Person. (Use the convinient Export to PostScript feature of Times.)
- Written description of your model.
- Verifcation queries you have used and their results (SATISFIED / NOT SATISFIED).
- The maximum brewing time.
- To get the expected behaviour from your system you need to declare all the communication channels, ie. coin, cof and pub, as urgent, (for example urgent chan coin). This will ensure that a transition is taken as soon as two interacting automata are ready to synchronize. Please observe that you can not have any clock guards on transitions which are synchronizing over urgent channels. You don't need to declare any locations as urgent or committed.
Verifier: Server Connection Lost Problem
To use the verifier you need to have at least one task in the system, even if you don't need any. You can just add one dummy periodic task with computation time 0 and period 10.
- Read the Times User Manual on verification and the Modelling Tips for Times.
- You may model the brewing as a task, but it is probably easier not to use any tasks in this model.
A Simple Protocol
The main purpose of this assignment is to practice modelling of a protocol with some real-time properties, and to get more familiar with the simulation of models.
You are asked to model a communication medium M, a Sender, and a Receiver.
The sender sends messages of a fixed length length, which is the time between the beginning and the end of a message. The medium has a transmission delay delay, which is the time between the beginning (or end) of a message is sent and the beginning (or end) of a message is received. For example, if the beginning of a message is sent at time t, it will be received by the receiver at time t+delay.
Task 1: Model the system as a network of timed automata in Times. Assume length>delay. Model the beginning and end of each message. It is recommended to use integer constants in Times for the values length and delay.
The Medium automaton should not be needing the length value to work correctly. Instead it only needs to synchronize with the other automata using the b = begin send, e = end send, br = begin receive and er = end receive communication channels.
The Receiver automaton should look like this.
Task 2: Validate the system in the simulator and find out what the
total timed between begin send and end receive is.
Task 3: Extend the medium M to also handle messages of length
What to report:
- Printouts of the models in all three tasks.
- Text describing your design.
- Total time between begin send and end receive.
Sporadic and periodic tasks
The main purpose of this assignmnet is to use Times to study scheduling of a task set. We are given a task set that contains both periodic and sporadic tasks. Some of the tasks also have conditions telling when they should run.
Make a model in Times that express the following task set.
|Q||C||1||(10-20)||20||(Period varies continuously between 10 and 20)|
|R||C||3||(20)||20||From time 20 to 100, periodic|
|T||C||2||(10)||10||When the last instance of R has finished and then periodically|
What to report:
- Model of the system
- Screen capture of the schedule (in the Simulator) for the first 150 time units.
To work at home you need to download the tool from the Times website: www.timestool.com.
When downloading please do us a favour and enter your real name and affiliation. To run Times you will also need a Java Runtime Environment version 1.4 or newer. There are several implementations of Java, for example Suns at java.sun.com.
A report is to be handed in for the assignment. It should include at least the following:
- The cover page.
- Answers to the given assignments (in part 2 all three task should be presented). These have three parts, the created timed automata, text describing how your timed automata are supposed to work and last (but not least) the verification queries used to answer the question.