 |
| |
|
[ updateable webserver example ] |
|
This section details an example of using Crowfoot to verify runtime updates. Specifically, we give an implementation,
in Crowfoot's input language, of the (idealised) updateable webserver from the paper "Formalizing Dynamic Software Updating" by Bierman,
Hicks, Sewell and Stoyle. We present Crowfoot input files for three versions, or stages, of the example.
-
Initial version:
Here we implement and prove the updateable webserver. This proof would be done before
we start the server running.
-
Version with one update:
Here we add to the code an update which adds logging, so that a record is kept of every event handled.
This proof would be done when the server is already running, once we have decided on the need for,
and programmed, the update.
-
Version with two updates:
This code includes the update to add logging, and then another, later update to change the type of events
handled, using the "convert" strategy to deal with events already in the queue. This proof would be done
when the server is running with the first update (to add logging) already in place, once we have programmed
the second update.
The following images show examples of the graphical output which Crowfoot can generate to explain its proofs.
They are taken from the proofs of the version with one update.
-
Graph 1:
This shows the symbolic execution of the 'update' procedure. One can see some ghost statements that
perform folding and unfolding of predicates, and one can see the nested triples appearing
in assertions as procedures are written to the heap.
-
Graph 2:
This shows the symbolic execution of the 'handle' procedure. One sees the branching of the symbolic
execution tree, produced by, among other things, if-then-else statements. Yellow nodes are where
the symbolic state was found to be inconsistent (and thus there was no further work to do). Green nodes
show where the end of the procedure body was reached, and an appropriate postcondition was proved to hold.
-
Graph 3:
This shows a proof of an entailment between assertions, which arises while checking the 'handle' procedure;
this proof obligation corresponds to the rightmost green box in Graph 2.
|
|
|
