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

1

X (sender's signal)

0

Hi

Signal on bus

Lo

1

Y (receiver's signaal)

0

1

R (Reliability)

0

r r

r r

Time

receiver's clock ticks

Fig. 2. Signal patterns

decoding function g , which maps a DC formula expressing the behaviour of Y
to a sequence of bits. The protocol is correct iff for any sequence w of bits, if
the sender puts the signal represented by f ( w ) on the bus then by digitising the
receiver must receive and receives only the signals represented by a DC formula
D for which g ( D )= w .

5.1 Biphase Mark Protocols

In the Biphase Mark Protocols (BMP) the sender encodes a bit as a cell con-
sisting of a mark subcell of length b and a code subcell of length a . The sender
keeps the signal stable in each subcell (hence either

X ¬ X

holds for the
interval representing a subcell). For a cell, if the signal in the mark subcell is
the same as the signal in the code subcell, the information carried by the cell is
0; otherwise, the information carried by the cell is 1. There is a phase reverse
between two consecutive cells. This means that, for a cell, the signal of the mark
subcell of the following cell is held as the negation of the signal of the code
subcell of the cell. The receiver, on detecting a state change (of Y ), knows that
it is the beginning of a cell, and skips d cycles (called the sampling distance )
and samples the signal. If the sampled signal is the same as the signal at the
beginning of the cell, it decodes the cell as 0; otherwise it decodes the cell as 1.
At the beginning of the transmission, the signal is low for a cycles (this means,

or

¬ holds for the interval of length a starting from the beginning). When the

sender finishes sending, it keeps the signal stable for cc time units which is longer
than the code subcell. We use HLS , LHS to denote the formulas representing
intervals consisting of the code subcell of a cell and the mark subcell of the next
one for the sender, and use HLR ( = d ), LHR ( = d ) to denote the formulas

X