Abstract
This chapter explores the relationship between testing and refinement. In particular, it looks at how tests for a refinement can be derived from tests for the abstract system. We discuss both how to derive tests from a formal specification, and also how tests can be refined for use with an implementation. We also consider how concrete tests can be calculated from abstract ones for refinements which are downward or upward simulations.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Excerpts from pp. 27–35, 38, 40–44, 46 of [13] are reprinted within this chapter with permission from John Wiley & Sons Limited.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Behnia, S., & Waeselynck, H. (1999) Test criteria definition for B models. In Wing et al. [32] (pp. 509–529).
Bloomfield, R., Marshall, L., & Jones, R. (Eds.) (1988). VDM’88. Lecture Notes in Computer Science: Vol. 328. Berlin: Springer.
Bowen, J. P., Fett, A., & Hinchey, M. G. (Eds.) (1998). ZUM’98: the Z Formal Specification Notation. Lecture Notes in Computer Science: Vol. 1493. Berlin: Springer.
Bowen, J. P. & Hinchey, M. G. (Eds.) (1995). ZUM’95: the Z Formal Specification Notation. Lecture Notes in Computer Science: Vol. 967. Limerick: Springer.
Bowen, J. P. & Nicholls, J. E. (Eds.) (1992). Seventh Annual Z User Workshop. London: Springer.
Brinksma, E. (1988). A theory for the derivation of tests. In S. Aggarwal & K. Sabnani (Eds.), Protocol Specification, Testing and Verification, VIII, Atlantic City, USA, June 1988 (pp. 63–74). Amsterdam: North-Holland.
Brinksma, E., Scollo, G., & Steenbergen, C. (1986). Process specification, their implementation and their tests. In B. Sarikaya & G. v. Bochmann (Eds.), Protocol Specification, Testing and Verification, VI, Montreal, Canada, June 1986 (pp. 349–360). Amsterdam: North-Holland.
Carrington, D., Maccoll, I., Mcdonald, J., Murray, L., & Strooper, P. (2000). From Object-Z specifications to ClassBench test suites. Journal on Software Testing, Verification and Reliability, 10(2), 111–137.
Carrington, D., & Stocks, P. (1998) A tale of two paradigms: Formal methods and software testing. In Bowen et al. [3] (pp. 51–68).
Cusack, E., & Wezeman, C. (1992) Deriving tests for objects specified in Z. In Bowen and Nicholls [5] (pp. 180–195).
de Nicola, R., & Hennessy, M. (1984). Testing equivalences for processes. Theoretical Computer Science, 34(3), 83–133.
Derrick, J., & Boiten, E. A. (1998) Testing refinements by refining tests. In Bowen et al. [3] (pp. 265–283).
Derrick, J., & Boiten, E. A. (1999). Testing refinements of state-based formal specifications. Software Testing, Verification & Reliability, 9, 27–50.
Dick, J., & Faivre, A. (1993). Automating the generation and sequencing of test cases from model-based specifications. In J. C. P. Woodcock & P. G. Larsen (Eds.), FME’93: Industrial-Strength Formal Methods. Lecture Notes in Computer Science: Vol. 428 (pp. 268–284). Berlin: Springer.
Grochtmann, M., & Grimm, K. (1993). Classification trees for partition testing. Software Testing, Verification & Reliability, 3, 63–82.
Hayes, I. J. (1986). Specification directed module testing. IEEE Transactions on Software Engineering, SE-12(1), 124–133.
Heerink, L., & Tretmans, J. (1997) Refusal testing for classes of transition systems with inputs and outputs. In Mizuno et al. [23] (pp. 23–38).
Hierons, R. M. (1997). Testing from a Z specification. Software Testing, Verification & Reliability, 7(1), 19–33.
Hierons, R. M., Bogdanov, K., Bowen, J. P., Cleaveland, R., Derrick, J., Dick, J., Gheorghe, M., Harman, M., Kapoor, K., Krause, P., Lüttgen, G., Simons, A. J. H., Vilkomir, S., Woodward, M. R., & Zedan, H. (2009). Using formal specifications to support testing. ACM Computing Surveys, 41(2), 9:1–9:76.
Hierons, R. M., Bowen, J. P., & Harman, M. (Eds.) (2008). Formal Methods and Testing, an Outcome of the FORTEST Network, Revised Selected Papers. Lecture Notes in Computer Science: Vol. 4949. Berlin: Springer.
Hinchey, M. G. & Liu, S. (Eds.) (1997). First International Conference on Formal Engineering Methods (ICFEM’97). Hiroshima, Japan, November 1997. Los Alamitos: IEEE Comput. Soc.
Hörcher, H.-M. (1995) Improving software tests using Z specifications. In Bowen and Hinchey [4] (pp. 152–166).
Mizuno, T., Shiratori, N., Higashino, T., & Togashi, A. (Eds.) (1997) FORTE/PSTV’97, Osaka, Japan, November 1997. London: Chapman & Hall.
Murray, L., Carrington, D., MacColl, I., McDonald, J., & Strooper, P. (1998) Formal derivation of finite state machines for class testing. In Bowen et al. [3] (pp. 42–59).
Murray, L., Carrington, D., Maccoll, I., & Strooper, P. (1999). Tinman—a test derivation and management tool for specification-based class testing. In International Conference on Technology of Object-Oriented Languages (TOOLS’99) (pp. 222–233). Los Alamitos: IEEE Comput. Soc.
Offutt, J., Liu, S., Abdurazik, A., & Ammann, P. (2003). Generating test data from state-based specifications. The Journal of Software Testing, Verification and Reliability, 13, 25–53.
Scullard, G. T. (1988) Test case selection using VDM. In Bloomfield et al. [2] (pp. 178–186).
Singh, H., Conrad, M., & Sadeghipour, S. (1997) Test case design based on Z and the classification-tree method. In Hinchey and Liu [21] (pp. 81–90).
Stepney, S. (1995) Testing as abstraction. In Bowen and Hinchey [4] (pp. 137–151).
Stocks, P. (1993). Applying formal methods to software testing. PhD thesis, Department of Computer Science, University of Queensland, St. Lucia, Australia.
van Aertryck, L., Benveniste, M., & Le Metayer, D. (1997) Casting: A formally based software test generation method. In Hinchey and Liu [21] (pp. 101–110).
Wing, J. M., Woodcock, J. C. P., & Davies, J. (Eds.) (1999). FM’99 World Congress on Formal Methods in the Development of Computing Systems. Lecture Notes in Computer Science: Vol. 1708. Berlin: Springer.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag London
About this chapter
Cite this chapter
Derrick, J., Boiten, E.A. (2014). Testing and Refinement. In: Refinement in Z and Object-Z. Springer, London. https://doi.org/10.1007/978-1-4471-5355-9_7
Download citation
DOI: https://doi.org/10.1007/978-1-4471-5355-9_7
Publisher Name: Springer, London
Print ISBN: 978-1-4471-5354-2
Online ISBN: 978-1-4471-5355-9
eBook Packages: Computer ScienceComputer Science (R0)