--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/example/Read_me Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,177 @@
+Isabelle Verification of a protocol using IOA.
+
+------------------------------------------------------------------------------
+The theory structure looks like this picture:
+
+ Correctness
+
+ Impl
+
+Sender Receiver Channels Spec
+
+ Action IOA Multisets
+
+ Packet List
+
+ Arith
+
+------------------------------------------------------------------------------
+
+The System.
+
+The system being proved correct is a parallel composition of 4 processes:
+
+ Sender || Schannel || Receiver || Rchannel
+
+Accordingly, the system state is a 4-tuple:
+
+ (Sender_state, Schannel_state, Receiver_state, Rchannel_state)
+
+------------------------------------------------------------------------------
+Packets.
+
+The objects going over the medium from Sender to Receiver are modelled
+with the type
+
+ 'm packet = bool * 'm
+
+This expresses that messages (modelled by polymorphic type "'m") are
+sent with a single header bit. Packet fields are accessed by
+
+ hdr<b,m> = b
+ mesg<b,m> = m
+------------------------------------------------------------------------------
+
+The Sender.
+
+The state of the process "Sender" is a 5-tuple:
+
+ 1. messages : 'm list (* sq *)
+ 2. sent : bool multiset (* ssent *)
+ 3. received : bool multiset (* srcvd *)
+ 4. header : bool (* sbit *)
+ 5. mode : bool (* ssending *)
+
+
+The Receiver.
+
+The state of the process "Receiver" is a 5-tuple:
+
+ 1. messages : 'm list (* rq *)
+ 2. replies : bool multiset (* rsent *)
+ 3. received : 'm packet multiset (* rrcvd *)
+ 4. header : bool (* rbit *)
+ 5. mode : bool (* rsending *)
+
+
+The Channels.
+
+The Sender and Receiver each have a proprietary channel, named
+"Schannel" and "Rchannel" respectively. The messages sent by the Sender
+and Receiver are never lost, but the channels may mix them
+up. Accordingly, multisets are used in modelling the state of the
+channels. The state of "Schannel" is modelled with the following type:
+
+ 'm packet multiset
+
+The state of "Rchannel" is modelled with the following type:
+
+ bool multiset
+
+This expresses that replies from the Receiver are just one bit.
+
+------------------------------------------------------------------------------
+
+The events.
+
+An `execution' of the system is modelled by a sequence of
+
+ <system_state, action, system_state>
+
+transitions. The actions, or events, of the system are described by the
+following ML-style datatype declaration:
+
+ 'm action = S_msg ('m) (* Rqt for Sender to send mesg *)
+ | R_msg ('m) (* Mesg taken from Receiver's queue *)
+ | S_pkt_sr ('m packet) (* Packet arrives in Schannel *)
+ | R_pkt_sr ('m packet) (* Packet leaves Schannel *)
+ | S_pkt_rs (bool) (* Packet arrives in Rchannel *)
+ | R_pkt_rs (bool) (* Packet leaves Rchannel *)
+ | C_m_s (* Change mode in Sender *)
+ | C_m_r (* Change mode in Receiver *)
+ | C_r_s (* Change round in Sender *)
+ | C_r_r ('m) (* Change round in Receiver *)
+
+------------------------------------------------------------------------------
+
+The Specification.
+
+The abstract description of system behaviour is given by defining an
+IO/automaton named "Spec". The state of Spec is a message queue,
+modelled as an "'m list". The only actions performed in the abstract
+system are: "S_msg(m)" (putting message "m" at the end of the queue);
+and "R_msg(m)" (taking message "m" from the head of the queue).
+
+
+------------------------------------------------------------------------------
+
+The Verification.
+
+The verification proceeds by showing that a certain mapping ("hom") from
+the concrete system state to the abstract system state is a `weak
+possibilities map` from "Impl" to "Spec".
+
+
+ hom : (S_state * Sch_state * R_state * Rch_state) -> queue
+
+The verification depends on several system invariants that relate the
+states of the 4 processes. These invariants must hold in all reachable
+states of the system. These invariants are difficult to make sense of;
+however, we attempt to give loose English paraphrases of them.
+
+Invariant 1.
+
+This expresses that no packets from the Receiver to the Sender are
+dropped by Rchannel. The analogous statement for Schannel is also true.
+
+ !b. R.replies b = S.received b + Rch b
+ /\
+ !pkt. S.sent(hdr(pkt)) = R.received(hdr(b)) + Sch(pkt)
+
+
+Invariant 2.
+
+This expresses a complicated relationship about how many messages are
+sent and header bits.
+
+ R.header = S.header
+ /\ S.mode = SENDING
+ /\ R.replies (flip S.header) <= S.sent (flip S.header)
+ /\ S.sent (flip S.header) <= R.replies header
+ OR
+ R.header = flip S.header
+ /\ R.mode = SENDING
+ /\ S.sent (flip S.header) <= R.replies S.header
+ /\ R.replies S.header <= S.sent S.header
+
+
+Invariant 3.
+
+The number of incoming messages in the Receiver plus the number of those
+messages in transit (in Schannel) is not greater than the number of
+replies, provided the message isn't current and the header bits agree.
+
+ let mesg = <S.header, m>
+ in
+ R.header = S.header
+ ==>
+ !m. (S.messages = [] \/ m ~= hd S.messages)
+ ==> R.received mesg + Sch mesg <= R.replies (flip S.header)
+
+
+Invariant 4.
+
+If the headers are opposite, then the Sender queue has a message in it.
+
+ R.header = flip S.header ==> S.messages ~= []
+