Abstract
One of the potential benefits of formal methods is that they offer the possibility of reducing the costs of testing. A specification acts as both the benchmark against which any implementation is tested, and also as the means by which tests are generated. There has therefore been interest in developing test generation techniques from formal specifications, and a number of different methods have been derived for state based languages such as Z, B and VDM. However, in addition to deriving tests from a formal specification, we might wish to refine the specification further before its implementation.
The purpose of this paper is to explore the relationship between testing and refinement. As our model for test generation we use a DNF partition analysis for operations written in Z, which produces a number of disjoint test cases for each operation. In this paper we discuss how the partition analysis of an operation alters upon refinement, and we develop techniques that allow us to refine abstract tests in order to generate test cases for a refinement. To do so we use (and extend existing) methods for calculating the weakest data refinement of a specification.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: The B-Book: Assigning programs to meanings. Cambridge University Press, Cambridge (1996)
Brinksma, E.: A theory for the derivation of tests. In: Aggarwal, S., Sabnani, K. (eds.) Protocol Specification, Testing and Verification VIII, Atlantic City, USA, pp. 63–74. North-Holland, Amsterdam (1988)
Brinksma, E., Scollo, G., Steenbergen, C.: Process specification, their implementation and their tests. In: Sarikaya, B., van Bochmann, G. (eds.) Protocol Specification, Testing and Verification VI, Montreal, Canada, pp. 349–360. North-Holland, Amsterdam (1986)
Carrington, D., Stocks, P.: A tale of two paradigms: Formal methods and software testing. In: Bowen, J.P., Hall, J.A. (eds.) Z User Workshop, Cambridge, June 1994, pp. 51–68 (1994)
Cusack, E., Wezeman, C.: Deriving tests for objects specified in Z. In: Bowen, J.P., Nicholls, J.E. (eds.) Z User Workshop, London. Workshops in Computing 1992, pp. 180–195. Springer, Heidelberg (1993)
de Nicola, R., Hennessy, M.: Testing equivalences for processes. Theoretical Computer Science 34(3), 83–133 (1984)
Derrick, J., Boiten, E.A.: Calculating and verifying refinements of state based specifications. Submitted of publication (1998)
Dick, J., Faivre, A.: Automating the generation and sequencing of test cases from model-based specifications. In: Larsen, P.G., Woodcock, J.C.P. (eds.) FME 1993. LNCS, vol. 670, pp. 268–284. Springer, Heidelberg (1993)
He, J.: Process refinement. In: McDermid, J. (ed.) The Theory and Practice of Refinement, Butterworths (1989)
Heerink, L., Tretmans, J.: Refusal testing for classes of transition systems with inputs and outputs. In: Mizuno, T., Shiratori, N., Higashino, T., Togashi, A. (eds.) FORTE/PSTV XVII 1997. Chapman and Hall, Boca Raton (1997)
Horcher, H.-M.: Improving software tests using Z specifications. In: Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1995. LNCS, vol. 967, pp. 152–166. Springer, Heidelberg (1995)
Jones, C.B.: Systematic Software Development using VDM. Prentice Hall International Series in Computer Science (1989)
Josephs, M.B.: The data refinement calculator for Z specifications. Information Processing Letters 27, 29–33 (1988)
Scullard, G.T.: Test case selection using VDM. In: Bloomfield, R.E., Jones, R.B., Marshall, L.S. (eds.) VDM 1988. LNCS, vol. 328, pp. 178–186. Springer, Heidelberg (1988)
Singh, H., Conrad, M., Sadeghipour, S.: Test case design based on Z and the classification-tree method. In: Hinchey, M.G., Liu, S. (eds.) First IEEE International Conference on Formal Engineering Methods (ICFEM 1997), Hiroshima, Japan, pp. 81–90. IEEE Computer Society Press, Los Alamitos (1997)
Smith, G., Derrick, J.: Refinement and verification of concurrent systems specified in Object-Z and CSP. In: Hinchey, M.G., Liu, S. (eds.) First IEEE International Conference on Formal Engineering Methods (ICFEM 1997), Hiroshima, Japan, pp. 293–302. IEEE Computer Society Press, Los Alamitos (1997)
Spivey, J.M.: The Z Notation: A Reference Manual. International Series in Computer Science (1989)
Stepney, S.: Testing as abstraction. In: Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1995. LNCS, vol. 967, Springer, Heidelberg (1995)
Stocks, P., Carrington, D.: Deriving software test cases from formal specifications. In: 6th Australian Software Engineering Conference, July 1991, pp. 327–340 (1991)
van Aertryck, L., Benveniste, M., Le Metayer, D.: Casting: A formally based software test generation method. In: Hinchey, M.G., Liu, S. (eds.) First IEEE International Conference on Formal Engineering Methods (ICFEM 1997), Hiroshima, Japan, pp. 101–110. IEEE Computer Society Press, Los Alamitos (1997)
Wezeman, C., Judge, A.J.: Z for managed objects. In: Bowen, J.P., Hall, J.A. (eds.) Z User Workshop, Cambridge. Workshops in Computing, pp. 108–119. Springer, Heidelberg (1994)
Woodcock, J.C.P., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science (1996)
Woodcock, J.C.P., Morgan, C.C.: Refinement of state-based concurrent systems. In: Langmaack, H., Hoare, C.A.R., Bjorner, D. (eds.) VDM 1990. LNCS, vol. 428, pp. 340–351. Springer, Heidelberg (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Derrick, J., Boiten, E. (1998). Testing Refinements by Refining Tests. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds) ZUM ’98: The Z Formal Specification Notation. ZUM 1998. Lecture Notes in Computer Science, vol 1493. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-49676-2_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-49676-2_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65070-6
Online ISBN: 978-3-540-49676-2
eBook Packages: Springer Book Archive