previous up next
Go backward to References
Go up to Top
RISC-Linz logo

A The Scheduler Protocol

The following specification does not yet incorporate the messages used for triggering the creation of a trace file (trace), for the generation of a trace label (label), for the creation of a visualization window (visual), for creating a shared data object (data), for writing such an object (put), and for having a task be executed by a separate process (proc).

In this section we formally specify the main part of the protocol by which an external application program communicates with the scheduler. The specification is expressed in the language of temporal logic [2] in the form

I => [] (A0 \/ ...\/ An)

which reads "if initially the condition I holds, then in every step one of the actions Ai is executed". Here we consider as an execution step the sending/receiving of a message from/to the scheduler; thus between two actions arbitrary real-time delays may occur.

An action is represented by a predicate Ai(V, V') that describes the relationship between the values V of the program variables before the action was performed and the corresponding values V' after completion of the action. An action

Action ==
/\

therefore increases the value of the program variable X by 1 and does not change the value of Y. As a convention, we omit all predicates that only demand that a variable does not change its value, i.e., whenever there is no other predicate V' = ... for some variable V in an action, we implicitly assume V' = V.

  • A.1 Protocol Variables
  • A.2 Message Passing
  • A.3 The Protocol

  • Maintainer: Wolfgang Schreiner
    Last Modification: July 6, 2001

    previous up next