ARTES
-------------------------------------------------

 

Formal Modelling and Analysis of Real-Time Systems: Lab 4

Part of the ARTES++ course Formella analysmetoder för realtidssystem (5p) VT'04.

Exercise 0

Installing the TIMES tool on your machine/account.

  1. Download TIMES from www.timestool.com.
  2. Follow the installation instructions.
  3. If there are problem, you might try to run TIMES manually. Then open a command shell in directory where TIMES is installed and run g:\program\j2sdk_nb\j2sdk1.4.2\bin\java -jar .\timestool.jar (where g:\program\j2sdk_nb\j2sdk1.4.2 is the path to your java installation).

Documentation: You may want to have a look at the documentation and the tutorials available on the TIMES web site.

Exercise 1

In this exercise you are asked to model and analyse a real-time system designed as a set of four tasks. The task paramters are shown in Table 1. Assume that preemptive scheduling is used.

Id Pri C D T
A 4 1 3 60
B 3 5 20 20
C 2 10 28 30
D 1 5 30 30

Table 1: Task Parameters.

Assignment 1: Simulate and perform schedulability analysis in TIMES. Use the defined priorities, and try also to simulate and perform schedulability analysis with the predefined scheduling strategies Rate Monotonic, Deadline Monotonic, Earliest Deadline First, and FIFO. Perform the analysis also for non-preemptive scheduling.

Assignment 2: Now modify the system so that task A is run periodically three times with deadline and period 4 every 50 time unit. Use a timed automaton with tasks to describe the release pattern of task A. Perform the analysis again (with preemptive scheduling).

Assignment 3: Now add the following behaviours of the tasks. This is done in the tab named Tasks.

  • Task B: multiply i by 2,
  • Task C: increment i by 1,
  • Task D: reset i if i>=32, and
  • Task A: in each burst (i.e. the four instances that are released every 50 time units) compute the sum of the three observed values of i.

where i is a shared integer variable. Simulate and analyse with preemptive scheduling policies.

Assignment 4: Now check if:

  • variable i can have a higher value than 50
  • variable i is always lower than 150

Assignment 5: Now introduce a precedence constraint requiring task D to precede task C. (Remember to enable the precedence constraint.) Analyse the two properties again.

  ---------------------line----------------------------
  Strategic Research