Quelle Overview.thy

Sprache: Isabelle

chapter ‹Isabelle Verification of a protocol using IOA›

theory Overview
imports IOA.IOA
begin

section ‹The System›

text ‹
system being proved correct is a parallel composition of 4 processes:

Sender || Schannel || Receiver || Rchannel

, the system state is a 4-tuple:

(Sender_state, Schannel_state, Receiver_state, Rchannel_state)
›

section ‹Packets›

text ‹
objects going over the medium from Sender to Receiver are modelled
the type

'm packet = bool × 'm

expresses that messages (modelled by polymorphic type ‹'m›) are
with a single header bit. Packet fields are accessed by

hdr<b,m> = b
mesg<b,m> = m
›

section ‹The Sender›

text ‹
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 *)
›

section ‹The Receiver›

text ‹
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 *)
›

section ‹The Channels›

text ‹
Sender and Receiver each have a proprietary channel, named
Schannel" and "Rchannel" respectively. The messages sent by the Sender
Receiver are never lost, but the channels may mix them
. Accordingly, multisets are used in modelling the state of the
. The state of "Schannel" is modelled with the following type:

'm packet multiset

state of "Rchannel" is modelled with the following type:

bool multiset

expresses that replies from the Receiver are just one bit.

Channels are instances of an abstract channel, that is modelled with
type

'a multiset.
›

section ‹The events›

text ‹
`execution' of the system is modelled by a sequence of

<system_state, action, system_state>

. The actions, or events, of the system are described by the
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 *)
›

section ‹The Specification›

text ‹
abstract description of system behaviour is given by defining an
/automaton named "Spec". The state of Spec is a message queue,
as an "'m list". The only actions performed in the abstract
are: "S_msg(m)" (putting message "m" at the end of the queue);
"R_msg(m)" (taking message "m" from the head of the queue).
›

section ‹The Verification›

text ‹
verification proceeds by showing that a certain mapping ("hom") from
concrete system state to the abstract system state is a `weak
map` from "Impl" to "Spec".

hom : (S_state * Sch_state * R_state * Rch_state) -> queue

verification depends on several system invariants that relate the
of the 4 processes. These invariants must hold in all reachable
of the system. These invariants are difficult to make sense of;
, we attempt to give loose English paraphrases of them.
›

subsection ‹Invariant 1›

text ‹
expresses that no packets from the Receiver to the Sender are
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)
›

subsection ‹Invariant 2›

text ‹
expresses a complicated relationship about how many messages are
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
›

subsection ‹Invariant 3›

text ‹
number of incoming messages in the Receiver plus the number of those
in transit (in Schannel) is not greater than the number of
, provided the message isn't current and the header bits agree.

let mesg = <S.header, m>
in
R.header = S.header
==>
∀m. (S.messages = [] ∨ m ≠ hd S.messages)
==> R.received mesg + Sch mesg ⊆ R.replies (flip S.header)
›

subsection ‹Invariant 4›

text ‹
the headers are opposite, then the Sender queue has a message in it.

R.header = flip S.header ==> S.messages ≠ []
›

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.