Specifying Various Time Models with Temporal Propositional Variables in Duration Calculus - Formal Methods and Hybrid Real-Time Systems - page 180

use temporal variable dLine i as in [2] whose behavior is similar to temporal
variable int , and specified by:

=0) ( dLine i = T i ) ∗ ) dLine i ⇒ (( dLine i ∧ ∧ ∧ (6)

= T i ) ∗ ( dLine i (( dLine i ∧ ∧ =0))

dLine i ( = T i ) ⇒ dLine i (7)

<T i (( dLine i = T i ) ∗ ∧ ≥

2 T i ⇒

∧

(8)

( true ( dLine i

= T i ) = T i ) ∗ ) ¬ ∧ ¬

( dLine i

∧ ∧

= T i ) ∗ ( dLine i = T i ) true )) ¬ ( ¬ ( dLine i ∧ ∧

<T i

Let Run i be a state variable saying that process i is running on the processor, i.e.
Run i ( t ) = 1 if process i is running on the processor, and Run i ( t )=0otherwise.
Let Stand i be a state variable saying that the current request of process i has
not been fulfilled. The behaviour of process i is fully specified by:

((( Run i <C i ⇔

) true ) dLine i ∧ = T i ⇒ Stand i ∧

( Run i = C i > 0 ⇒ Run i = C i ¬ Stand i ))

The requirement of system T is simply specified by: for all i ≤ n ,

= T i ⇒ Run i = C i

dLine i ∧

Formulas 6, 7 and 8 form a complete specification of temporal propositional
variables dLine i , i n , and are useful in proving the correctness of a scheduler

for system T . A priority-based scheduler

≤

for system T with single processor
is characterised by state variables HiPri ij ( i, j

S

≤ n, i = j ) which specify the

dynamic priority among the processes defined by S , and the following state

formulas characterising its behaviour:

∧ i = j (( Run i ∧ Stand j )= >HiPri ij )

∧ i≤n ( Run i = >Stand i )
∧ i = j ( HiPri ij ⇒¬

HiPri ji )
∧ i = j ¬ ( Run i ∧ Run j )
∨ i≤n Stand i ⇒∨ i≤n Run i

A deadline driven scheduler is a priority-based scheduler that considers process
i to have a higher prioity than process j (i.e. the value of HiPri ij at the current
time point is 1) iff the deadline for process i is nearer than the deadline for process
j . The deadline driven scheduler can be modelled in a much more convenient
way than in [2] with the additional formula specifying the behaviour of state
variables HiPri ij ( i, j ≤ n ):

= T i ⇒

dLine j ) dLine i true

∧ i = j HiPri ij ( ¬

The interesting thing here is that variables HiPri ij canbedefinedinDC,with-
out any quantification on rigid variables, via temporal propositional variables