src/HOL/HOLCF/IOA/NTP/Overview.thy

+chapter \<open>Isabelle Verification of a protocol using IOA\<close>
+
+theory Overview
+  imports IOA.IOA
+begin
+
+section \<open>The System\<close>
+
+text \<open>
+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)
+\<close>
+
+
+section \<open>Packets\<close>
+
+text \<open>
+The objects going over the medium from Sender to Receiver are modelled
+with the type
+
+    'm packet = bool \<times> 'm
+
+This expresses that messages (modelled by polymorphic type \<open>'m\<close>) are
+sent with a single header bit. Packet fields are accessed by
+
+    hdr<b,m> = b
+    mesg<b,m> = m
+\<close>
+
+
+section \<open>The Sender\<close>
+
+text \<open>
+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 *)
+\<close>
+
+
+section \<open>The Receiver\<close>
+
+text \<open>
+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 *)
+\<close>
+
+
+section \<open>The Channels\<close>
+
+text \<open>
+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.
+
+Both Channels are instances of an abstract channel, that is modelled with
+the type
+
+    'a multiset.
+\<close>
+
+
+section \<open>The events\<close>
+
+text \<open>
+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         *)
+\<close>
+
+
+section \<open>The Specification\<close>
+
+text \<open>
+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).
+\<close>
+
+
+section \<open>The Verification\<close>
+
+text \<open>
+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.
+\<close>
+
+
+subsection \<open>Invariant 1\<close>
+
+text \<open>
+This expresses that no packets from the Receiver to the Sender are
+dropped by Rchannel. The analogous statement for Schannel is also true.
+
+    \<forall>b. R.replies b = S.received b + Rch b
+    \<and>
+    \<forall>pkt. S.sent(hdr(pkt)) = R.received(hdr(b)) + Sch(pkt)
+\<close>
+
+
+subsection \<open>Invariant 2\<close>
+
+text \<open>
+This expresses a complicated relationship about how many messages are
+sent and header bits.
+
+    R.header = S.header
+    \<and> S.mode = SENDING
+    \<and> R.replies (flip S.header) \<subseteq> S.sent (flip S.header)
+    \<and> S.sent (flip S.header) \<subseteq> R.replies header
+    OR
+    R.header = flip S.header
+    \<and> R.mode = SENDING
+    \<and> S.sent (flip S.header) \<subseteq> R.replies S.header
+    \<and> R.replies S.header \<subseteq> S.sent S.header
+\<close>
+
+
+subsection \<open>Invariant 3\<close>
+
+text \<open>
+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
+    \<Longrightarrow>
+    \<forall>m. (S.messages = [] \<or> m \<noteq> hd S.messages)
+        \<Longrightarrow> R.received mesg + Sch mesg \<subseteq> R.replies (flip S.header)
+\<close>
+
+
+subsection \<open>Invariant 4\<close>
+
+text \<open>
+If the headers are opposite, then the Sender queue has a message in it.
+
+    R.header = flip S.header \<Longrightarrow> S.messages \<noteq> []
+\<close>
+
+end