Decoding Stream

One agent puts repeatedly pairs < bit, d > of bits and encoded datas into a channel which automatically decodes the information. When the agent reads < bit', d' > from the channel such that bit = bit', it is a confirmation that the data sent for decoding was received. In thad case, the agent stores the data received into a list structure, alternates the bit, and selects the next encoded data for sending. We assume that the channel is unreliable, meaning that the data in the channel may be lost or duplicated, but not exchanged or damaged.

Specification

See ds.maude for the full specification.

Verification

For the verification of the Decoding Stream, we are interested in two properties.

If the channel contains bit, then all the bits after bit are equal to bit.

DS |- ceq B':Bit = bit(S:Sys) if C1:Channel, < B:Bit,D:Data >, C2:Channel, < B':Bit,D':Data >, C3:Channel := channel(S:Sys) /\ B:Bit = bit(S:Sys) ;

See proof1.maude for the full proof.

All encrypted data sent are decoded and stored in the list structure in the same order in which they were sent.

DS |- eq mk(next(S:Sys)) = data(next(S:Sys)), list(S:Sys) ;

See proof2.maude for the full proof.