Validating Z specifications using the PROB animator and model checker

Abstract

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. © Springer-Verlag Berlin Heidelberg 2007.