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:

• the starting Z specification, paperexample.txt
• the translated SAL main context, paperexample.sal
• a trace where we found a Z specification error, papertrace.txt
• some timing data for LTL model-checking, papertimes.txt

In addition, the following library contexts were used:

• set.sal — for sets and finite sets
• count12.sal — for counting sets with max 12 elements
• relation.sal — for additional operations on relations
• function.sal — for partial and total functions

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!

• the (old) translated SAL main context, paperexample_old.sal
• some (old) timing data for LTL model-checking, papertimes_old.txt

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:

• the abstract Z specification, enterleave_set.txt
• the concrete Z specification, enterleave_seq.txt
• the retrieve relation, enterleave.txt
• the merged automaton for checking initialisation, enterleave_init.sal
• the merged automaton for checking applicability and correctness, enterleave_app_corr.sal

In addition, the following library contexts were used:

• set.sal — for sets and finite sets
• count3.sal — for counting sets with max 3 elements
• sequence.sal — for sequences indexed by positive naturals

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:

• the abstract Z specification, marlowe.txt
• the concrete Z specification, kurbel.txt
• the retrieve relation, tickets.txt
• the merged automaton for checking initialisation, tickets_init.sal
• the merged automaton for checking applicability and correctness, tickets_app_corr.sal

In addition, the following library contexts were used:

• set.sal — for sets and finite sets

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.