1Isabelle Verification of a protocol using IOA. 2 3------------------------------------------------------------------------------ 4 5The System. 6 7The system being proved correct is a parallel composition of 4 processes: 8 9 Sender || Schannel || Receiver || Rchannel 10 11Accordingly, the system state is a 4-tuple: 12 13 (Sender_state, Schannel_state, Receiver_state, Rchannel_state) 14 15------------------------------------------------------------------------------ 16Packets. 17 18The objects going over the medium from Sender to Receiver are modelled 19with the type 20 21 'm packet = bool * 'm 22 23This expresses that messages (modelled by polymorphic type "'m") are 24sent with a single header bit. Packet fields are accessed by 25 26 hdr<b,m> = b 27 mesg<b,m> = m 28------------------------------------------------------------------------------ 29 30The Sender. 31 32The state of the process "Sender" is a 5-tuple: 33 34 1. messages : 'm list (* sq *) 35 2. sent : bool multiset (* ssent *) 36 3. received : bool multiset (* srcvd *) 37 4. header : bool (* sbit *) 38 5. mode : bool (* ssending *) 39 40 41The Receiver. 42 43The state of the process "Receiver" is a 5-tuple: 44 45 1. messages : 'm list (* rq *) 46 2. replies : bool multiset (* rsent *) 47 3. received : 'm packet multiset (* rrcvd *) 48 4. header : bool (* rbit *) 49 5. mode : bool (* rsending *) 50 51 52The Channels. 53 54The Sender and Receiver each have a proprietary channel, named 55"Schannel" and "Rchannel" respectively. The messages sent by the Sender 56and Receiver are never lost, but the channels may mix them 57up. Accordingly, multisets are used in modelling the state of the 58channels. The state of "Schannel" is modelled with the following type: 59 60 'm packet multiset 61 62The state of "Rchannel" is modelled with the following type: 63 64 bool multiset 65 66This expresses that replies from the Receiver are just one bit. 67 68Both Channels are instances of an abstract channel, that is modelled with 69the type 70 71 'a multiset. 72 73------------------------------------------------------------------------------ 74 75The events. 76 77An `execution' of the system is modelled by a sequence of 78 79 <system_state, action, system_state> 80 81transitions. The actions, or events, of the system are described by the 82following ML-style datatype declaration: 83 84 'm action = S_msg ('m) (* Rqt for Sender to send mesg *) 85 | R_msg ('m) (* Mesg taken from Receiver's queue *) 86 | S_pkt_sr ('m packet) (* Packet arrives in Schannel *) 87 | R_pkt_sr ('m packet) (* Packet leaves Schannel *) 88 | S_pkt_rs (bool) (* Packet arrives in Rchannel *) 89 | R_pkt_rs (bool) (* Packet leaves Rchannel *) 90 | C_m_s (* Change mode in Sender *) 91 | C_m_r (* Change mode in Receiver *) 92 | C_r_s (* Change round in Sender *) 93 | C_r_r ('m) (* Change round in Receiver *) 94 95------------------------------------------------------------------------------ 96 97The Specification. 98 99The abstract description of system behaviour is given by defining an 100IO/automaton named "Spec". The state of Spec is a message queue, 101modelled as an "'m list". The only actions performed in the abstract 102system are: "S_msg(m)" (putting message "m" at the end of the queue); 103and "R_msg(m)" (taking message "m" from the head of the queue). 104 105 106------------------------------------------------------------------------------ 107 108The Verification. 109 110The verification proceeds by showing that a certain mapping ("hom") from 111the concrete system state to the abstract system state is a `weak 112possibilities map` from "Impl" to "Spec". 113 114 115 hom : (S_state * Sch_state * R_state * Rch_state) -> queue 116 117The verification depends on several system invariants that relate the 118states of the 4 processes. These invariants must hold in all reachable 119states of the system. These invariants are difficult to make sense of; 120however, we attempt to give loose English paraphrases of them. 121 122Invariant 1. 123 124This expresses that no packets from the Receiver to the Sender are 125dropped by Rchannel. The analogous statement for Schannel is also true. 126 127 !b. R.replies b = S.received b + Rch b 128 /\ 129 !pkt. S.sent(hdr(pkt)) = R.received(hdr(b)) + Sch(pkt) 130 131 132Invariant 2. 133 134This expresses a complicated relationship about how many messages are 135sent and header bits. 136 137 R.header = S.header 138 /\ S.mode = SENDING 139 /\ R.replies (flip S.header) <= S.sent (flip S.header) 140 /\ S.sent (flip S.header) <= R.replies header 141 OR 142 R.header = flip S.header 143 /\ R.mode = SENDING 144 /\ S.sent (flip S.header) <= R.replies S.header 145 /\ R.replies S.header <= S.sent S.header 146 147 148Invariant 3. 149 150The number of incoming messages in the Receiver plus the number of those 151messages in transit (in Schannel) is not greater than the number of 152replies, provided the message isn't current and the header bits agree. 153 154 let mesg = <S.header, m> 155 in 156 R.header = S.header 157 ==> 158 !m. (S.messages = [] \/ m ~= hd S.messages) 159 ==> R.received mesg + Sch mesg <= R.replies (flip S.header) 160 161 162Invariant 4. 163 164If the headers are opposite, then the Sender queue has a message in it. 165 166 R.header = flip S.header ==> S.messages ~= [] 167 168