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

Sender Receiver

decode

encode

received signal

sent signal

Digitizing

Bus

Receiver clock

Fig. 1. Communication Protocol Model

The communication protocols are modelled in DC as follows. The signal sent
by the sender is modelled by a state X . The signal received by the receiver by
sampling the signal on the bus is modelled by a state Y in the sampling time
model with the sampling time step 1. So, step = 1. However, it is not

the case that samp ( X, Y ) due to the fact that it takes a significant amount of
time to change the signal on the bus from high to low or vice-versa, and hence,
the signal on the bus cannot be represented by a Boolean function. Without loss
of generality, assume that the delay between the sender and the receiver is 0.
Assume also that when the signal on the bus is neither high nor low, the receiver
will choose an arbitrary value from

⇔ int ∧

for the value of Y . The phenomenon
is depicted in Fig. 2. Assume that it takes r ( r is a natural number) receiver-
clock cycles for the sender to change the signal on the bus from high to low
or vice-versa. Then if the sender changes the signal from low to high or from
high to low, the receiver's signal will be unreliable for r cycles starting from the
last tick of the receiver clock and during this period it can be any value chosen
nondeterministically from 0 and 1. Otherwise, the signal received by the receiver
is the same as the signal sent by the sender (see Figure 2). This relationship
between X and Y is formalised as

{ 0 , 1 }

r ) ( int ) ( < 1) ,

( X ∧ ( ≥ r +1)) ⇒ ( ≤ Y ∧

r ) ( int ) ( < 1) .

( ¬ X ∧ ( ≥ r +1)) ⇒ ( ≤ ¬ Y ∧

Since the behaviour of a state can be specified by a DC formula, a commu-
nication protocol can be modelled as consisting of a coding function f ,which
maps a sequence of bits to a DC formula expressing the behaviour of X ,anda