Model-Checking
The Z2SAL translator can generate a SAL automaton for a single Z
specification, in which every Z operation schema becomes a transition
represented as a guarded command. It is possible to add LTL theorems
to the end of this automaton, to check whether certain properties
always hold, or eventually hold. The translator may also be used to
generate a merged SAL automaton for two Z specifications that are
related by a retrieve relation. It is possible to add CTL theorems
to the end of this automaton, to check for refinement between the
two original specifications.
Simulation and Model-Checking Tools
The output produced by the Z2SAL translator may be simulated directly
in the SAL simulator. Alternatively, you may add further temporal logic
properties in LTL or CTL (by hand) at the end of the main context, for
model-checking or refinement checking purposes. The SAL tools we use
most frequently are:
sal-sim — the interactive simulator
sal-smc — the simple model checker (LTL)
sal-bmc — the bounded model checker (LTL)
sal-wmc — the witness model checker (CTL)
To obtain these tools, you should visit SRI's website for the
Symbolic Analysis Laboratory (SAL), from where you may download
the latest version of the SAL tool suite.
Simulation and Model-Checking
Here is an example we used in the FAoC 23(1), 2011 paper.
It concerns
a video shop, where it is possible for customers to become members and
then to rent videos. The example exercises sets, functions and relations
from the Z mathematical toolkit.
The SAL was generated here by the latest version
of our Z2SAL translator, and is considerably more efficient than the original published version (compared below).
Several anciliary library context files were also generated (see the
Z Mathematical
Toolkit for further details), as shown below.
Video Shop Example
This example may be simulated in sal-sim , using the above
main context and suitable library context files. Subsequently, seven
temporal logic
formulae in LTL were added by hand (indicated in the SAL file).
These are expressed as counter-theorems, asserting a negative
property, in order to force the model-checker to demonstrate a positive
counter-example. These theorems may be checked in the model-checker
sal-smc to reveal the counter-examples. We provide below:
In addition, the following library contexts were used:
Note that the timing data supplied is for the latest translation. For
comparison, we show below the original SAL translation that was published
in the FAoC 23(1), 2011 paper,
and the timing data for the same LTL theorems. The new translation affords
a speed improvement of about one order of magnitude!
You should be able to download the original Z specification, and
translate it in the Z2SAL tool; then if you add theorems in the style
illustrated, you can model-check the generated result.
Checking a Refinement Relation
Here are some examples we use in the forthcoming FAoC paper.
It concerns a simple sign-in system for a club, in which members may enter
or leave. The abstract specification describes this using sets, whereas a
concrete specification describes this using an injective sequence. The
SAL was generated by the internal alpha-version of our translator, which
can also handle Z sequences, and yields one context for checking
the initialisation theorem, and another context for checking the
applicability and correctness theorems. The first example also exercises
the new sequence encoding.
Enter/Leave Set and Sequence Example
This example may be simulated in sal-sim ,
using the main context and suitable library context files,
which were generated automatically (see below). Subsequently, the
initialisation, applicability and correctness theorems in CTL were
added by hand to the respective contexts (indicated in the SAL
files). These may be checked in the sal-wmc witness model
checker, which issues a single VALID or INVALID
judgement and drops the user into an interactive mode, in which you may
explore the labelled transition system. We provide below:
In addition, the following library contexts were used:
Note that for checking applicability and correctness, you may check the
whole specification in one go (first two theorems), or check each operation
refinement individually (all the remaining theorems), depending on how you
choose to express the CTL theorems.
Kurbel and Marlowe Theatre Booking Example
This classic example from the refinement literature may be simulated
in sal-sim , using the main
context and suitable library context files, which were
generated automatically (see below). Subsequently, the
initialisation, applicability and correctness theorems in CTL were
added by hand to the respective contexts (indicated in the SAL
files). These may be checked in the sal-wmc witness model
checker, which issues a single VALID or INVALID
judgement and drops the user into an interactive mode, in which you may
explore the labelled transition system. We provide below:
In addition, the following library contexts were used:
You should be able to download the original Z LaTeX
files and translate these, using our Z2SAL translator.
If you model-check the three theorems, you should find
that whereas initialisation and
correctness are valid, the applicability check fails, due to a
hard-to-detect condition discussed in the paper, which previous
authors have failed to spot. This demonstrates the usefulness
of automated refinement checking.
|