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