Real-Time Systems

Lecture 4

Subject

Semantics of TCTL
Region Automata
Basic Decidability Results

Material

Continuous Modeling of Real Time and Hybrid Systems (focus on section 5).
JPK chapter4: sections 4.4 to 4.8 (skim sections 4.6 and 4.7).

Slides.

Exercises

Exercise 1 (Modeling)

JPK exercise 32.

Exercise 2 (Theory)

JPK exercises 26, 30, 31.2-3.

Exercise 3 (Modeling)

In this exercise we study Fischer's protocol for mutual exclusion in more detail. We start out from the version presented at todays lecture, which is given in the files fischer.xta and fischer.ugi.
 

Figure 1: Simplified Model of Fischer's Protocol.

 

Task 1: Use the verifier of UPPAAL to check if the protocol satisfies the following requirements:

1. mutual exclusion, i.e. that there is never more than one process operating in its critical section (modeled by location cs),
2. all processes can enter their critical sections, and
3. a process is guaranteed to enter its critical location within three time units.

Task 2: The protocol model is slightly inaccurate as the processes can not leave the critical section. Refine the protocol to allow processes to restart after having gained access to the critical section and after having failed to gain access to the critical section. Rerun the verification.

Task 3: The protocol model is still slightly inaccurate as a process may stay too long in location b and will therefore not be able to eventually reach the critical section. Refine the protocol to model the fact that processes may, or may not, be interested in accessing the critical section. Make sure that a process is always is allowed to eventually reach the critical section. Rerun the verification.