diff -r f04b33ce250f -r a4dc62a46ee4 IOA/example/Read_me --- 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 - mesg = 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 - - - -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 = - 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 ~= [] -