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