--- a/IOA/example/Read_me Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,177 +0,0 @@
-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 ~= []
-