Validating Z Specifications Using the ProB Animator and Model Checker

We present the architecture and implementation of the

proz

tool to validate high-level Z specifications. The tool was integrated into

prob

, by providing a translation of Z into B and by extending the kernel of

prob

to accommodate some new syntax and data types. We describe the challenge of going from the tool friendly formalism B to the more specification-oriented formalism Z, and show how many Z specifications can be systematically translated into B. We describe the extensions, such as record types and free types, that had to be added to the kernel to support a large subset of Z. As a side-effect, we provide a way to animate and model check records in

prob

. By incorporating

proz

into

prob

, we have inherited many of the recent extensions developed for B, such as the integration with CSP or the animation of recursive functions. Finally, we present a successful industrial application, which makes use of this fact, and where

proz

was able to discover several errors in Z specifications containing higher-order recursive functions.