Formal Specification and Proofs for Isolated Protocols
This page documents the KIV specifications and the formal proofs that justify the results of
Section 3 of the paper Atomic Actions, and their Refinements to Isolated and Not-So-Isolated Protocols
by Richard Banach and Gerhard Schellhorn, submitted to FAC (available from the authors). This page should be read in conjunction
with Section 10 of the paper, which gives some information on the formal specification.
To get an overview over the structure of the specifications you can have a look at the
development graph. This page gives a bottom-up overview over the content of the specifications.
- Specification
Step gives the step relation St of atomic steps of protocols and defines initial and final states.
- Based on a
free data type we then specify predicates Path, FPath, BPath and MPath. Predicate Path holds, if every step of the path is in the step relation St,
FPaths (forward paths) additionally start with an initial state. BPaths (backward paths) have a final state as the last one,
and MPath (maximal path) holds if the path is both an FPath and a BPath. The specification also defines a number of operations
on paths like selecting the nth step, selecting the nth node, the length of the path etc. and proves suitable lemmas that are used as simplifier rules to have a decent automation for proofs.
- For maximal paths a
synchronization assigment is defined, by specifying a function SA on MPaths. Mpath(pa) is the position of the synchronization step on the path pa. The function is specified by two constraints: the synchronisation step must be on the path (of course), and for two paths, which have a state in common, the synchronization assignment must select for both paths either a step that is before the common node, or one after the common node.
- Based on
atomic abstract steps and a definition of
protocols we can then define the 'ASM style'
big step proof obligation. The past oriented and the future oriented simulation
relations are also defined in
this specification.
Proposition 3.3 and Theorem 3.4 are proved.
- We then
define the simulation relation R1 and prove the main lemmas FS-BW, FS-FW etc. as described in the paper.
- Finally the
main theorems of section 3 are proved:
- Theorem 3.8, which characterizes the steps that can be simulated forwards and backwards,
- Corollary 3.9, which guarantees that backward simulation is always possible, and
- Corollary 3.10, which guarantees that forward simulation is always possible for a synchronization
assignment which always chooses the last step of each maximal path.
Used basic libraries:
Here you can find all our publications .
Back to the overview of all KIV projects .
For general informations on KIV and a download site for the whole system refer to this page.
[Impressum]
[E-Mail]