-- Multiplexed buffers, version for fdr.1.1 -- Bill Roscoe -- Modified for fdr.1.2 10/8/92 Dave Jackson -- The idea of this example is to multplex a number of buffers down a -- pair of channels. They can all be in one direction, or there might be -- some both ways. The techniques demonstrated here work for all -- numbers of buffers, and any types for transmission. The number of states -- in the system can be easily increased to any desired size by increasing -- either the number of buffers, or the size of the transmitted type. datatype Tag = t1 | t2 | t3 datatype Data = d1 | d2 channel left, right : Tag.Data channel snd_mess, rcv_mess : Tag.Data channel snd_ack, rcv_ack : Tag channel mess : Tag.Data channel ack : Tag -- The following four processes form the core of the system -- -- -- --> SndMess --> ........... --> RcvMess --> -- -- <-- RcvAck <-- ........... <-- SndAck <-- -- -- SndMess and RcvMess send and receive tagged messages, while -- SndAck and RcvAck send and receive acknowledgements. SndMess = [] i:Tag @ (snd_mess.i ? x -> mess ! i.x -> SndMess) RcvMess = mess ? i.x -> rcv_mess.i ! x -> RcvMess SndAck = [] i:Tag @ snd_ack.i -> ack ! i -> SndAck RcvAck = ack ? i -> rcv_ack.i -> RcvAck -- These four processes communicate with equal numbers of transmitters (Tx) -- and receivers (Rx), which in turn provide the interface with the -- environment. Tx(i) = left.i ? x -> snd_mess.i ! x -> rcv_ack.i -> Tx(i) Rx(i) = rcv_mess.i ? x -> right.i ! x -> snd_ack.i -> Rx(i) FaultyRx(i) = rcv_mess.i ? x -> right.i ! x ->(FaultyRx(i) |~| snd_ack.i -> FaultyRx(i)) -- Txs is the collection of transmitters working independently Txs = ||| i:Tag @ Tx(i) -- LHS is just everything concerned with transmission combined, with -- internal communication hidden. LHS = (Txs [|{|snd_mess, rcv_ack|}|](SndMess ||| RcvAck))\{|snd_mess, rcv_ack|} -- The receiving side is built in a similar way. Rxs = ||| i:Tag @ Rx(i) FaultyRxs = Rx(t1) ||| Rx(t2) ||| FaultyRx(t3) RHS = (Rxs [|{|rcv_mess, snd_ack|}|] (RcvMess ||| SndAck))\{|rcv_mess, snd_ack|} FaultyRHS = (FaultyRxs [|{|rcv_mess, snd_ack|}|] (RcvMess ||| SndAck))\{|rcv_mess, snd_ack|} -- Finally we put it all together, and hide internal communication System = (LHS [|{|mess, ack|}|] RHS)\{|mess,ack|} FaultySystem = (LHS [|{|mess, ack|}|] FaultyRHS)\{|mess, ack|} -- The specification is just the parallel composition of several one-place -- buffers. Copy(i) = left.i ? x -> right.i ! x -> Copy(i) Spec = ||| i:Tag @ Copy(i) -- Correctness of the system is asserted by Spec [FD= System. assert Spec [FD= System -- If the multiplexer is being used as part of a larger system, then -- it would make a lot of sense to prove that it meets its specification -- and then use its specification in its stead in higher-level system -- descriptions. This applies even if the higher-level system does not -- break up into smaller components, since the state-space of the -- specification is significantly smaller than that of the multiplexer, -- which will make the verification of a large system quicker. It is -- even more true if the channels of the multiplexer are used independently, -- in other words if each external channel of the multiplexer is connected -- to a different user, and the users do not interact otherwise, -- for it would then be sufficient to prove that each of the separate -- pairs of processes interacting via our multiplexer are correct relative -- to its own specification, with a simple one-place buffer between them. -- For we would have proved the equivalence, by the correctness of the -- multiplexer, of our system with a set of three-process independent ones.
Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.