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 modelchecking. 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.
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 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.
