Journal Title
Title of Journal:
|
|
Publisher
Springer, Berlin, Heidelberg
|
|
|
|
Authors: Daniel Plagge Michael Leuschel
Publish Date: 2007/7/2
Volume: , Issue: , Pages: 480-500
Abstract
We present the architecture and implementation of the proz tool to validate highlevel 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 specificationoriented 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 sideeffect 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 higherorder recursive functions
Keywords:
.
|
Other Papers In This Journal:
|