Abstract
We use a structure preserving encoding of Z in the higher-order logic instance of the generic theorem prover Isabelle to derive test cases from Z specifications. This work shows how advanced theorem provers can be used with little effort to provide tool support for Z beyond mere type-checking. Experience with a non-trivial example shows that modular reasoning according to the structure of a specification is crucial to keep the proof-load manageable in practical applications. Support for modular reasoning can be based on higher-order equational reasoning as implemented in Isabelle.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J. P. Bowen and J. A. Hall, editors. Z User Workshop, Workshops in Computing. Springer Verlag, 1994.
J. P. Bowen and M. G. Hinchey, editors. ZUM'95: The Z Formal Specification Notation, LNCS 967. Springer Verlag, 1995.
R. Büssow and M. Weber. A Steam-Boiler Control Specification using Statecharts and Z. In J. R. Abrial, editor, Formal methods for industrial applications: specifying and programming the Steam Boiler Control, LNCS 1165. Springer Verlag, 1996.
E. Cusack and G. H. B. Rafsanjani. ZEST. In S. Stepney, R. Barden, and D. Cooper, editors, Object-Orientation in Z, Workshops in Computing. Springer Verlag, 1992.
J. Dick and A. Faivre. Automating the generation and sequencing of test cases from model-based specifications. In Woodcock and Larsen [17], pages 268–284.
M.-C. Gaudel. Testing can be formal, too. In P. D. Mosses, M. Nielsen, and M. I. Schwartzbach, editors, TAPSOFT '95: Theory and Practice of Software Development, LNCS 915, pages 82–96. Springer Verlag, 1995.
M. J. C. Gordon and T. M. Melham. Introduction to HOL: A theorem proving environment for higher order logics. Cambridge University Press, 1993.
H.-M. Hörcher. Improving software tests using Z specifications. In Bowen and Hinchey [2], pages 152–166.
Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle/HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher-Order Logics, LNCS 1125, pages 283–298. Springer Verlag, 1996.
E. Mikk. Compilation of Z specifications into C for automatic test result evaluation. In Bowen and Hinchey [2], pages 167–180.
J. Nicholls. Z Notation — version 1.2. Draft ISO standard, 1995.
L. C. Paulson. Isabelle — A Generic Theorem Prover. LNCS 828. Springer Verlag, 1994.
H. Singh, M. Conrad, G. Egger, and S. Sadeghipour. Tool-supported test case design based on Z and the classification-tree method, 1996. Proc. Second Workshop on Systems for Computer-Aided Specification, Development and Verification, to appear.
J. M. Spivey. The Fcuzz manual. Computing Science Consultancy, Oxford, UK, 1992.
J. M. Spivey. The Z Notation — A Reference Manual. Prentice Hall, 2nd edition, 1992.
S. Stepney. Testing as abstraction. In Bowen and Hinchey [2], pages 137–151.
J. C. P. Woodcock and P. G. Larsen, editors. FME '93: Industrial-Strength Formal Methods, LNCS 670. Springer Verlag, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Helke, S., Neustupny, T., Santen, T. (1997). Automating test case generation from Z specifications with Isabelle. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds) ZUM '97: The Z Formal Specification Notation. ZUM 1997. Lecture Notes in Computer Science, vol 1212. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027283
Download citation
DOI: https://doi.org/10.1007/BFb0027283
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62717-3
Online ISBN: 978-3-540-68490-9
eBook Packages: Springer Book Archive