Modeling and Verification of Concurrent Real-Time Systems: Lab 4

Exercise 0

Installing the TIMES tool on your machine/account. The TIMES tool is a vailable from www.timestool.com. Java is also required.

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 three 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.