A Look Inside

Here, we give some examples of the SAL context files generated by the Z2SAL translator, and show how LTL and CTL theorems can be added to these in order to perform model-checking. Also, we provide copies of the latest library context files used to model the Z mathematical toolkit in SAL. These files are automatically generated by the Z2SAL translator, when the specification needs them.

Model-Checking Examples

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.

The Z Mathematical Toolkit

The Z notation provides a rich foundation of mathematical datatypes, including sets, relations, functions, sequences and bags. Since these are frequently used in Z specifications, we implemented one or more SAL library contexts to model each datatype. Each context is parameterised by one or more types, affording reuse of each context to model many different typed constructions, by instantiating the parameters with different types.