Skip to main content

Testing refinements by refining tests

Derrick, John and Boiten, Eerke Albert (1998) Testing refinements by refining tests. In: Bowen, Jonathan P. and Fett, A. and Hinchey, Michael G., eds. ZUM ’98: The Z Formal Specification Notation 11th International Conference of Z Users. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 265-283. ISBN 978-3-540-65070-6. E-ISBN 978-3-540-49676-2. (doi:10.1007/978-3-540-49676-2_19) (KAR id:17694)

Language: English
Click to download this file (218kB)
[thumbnail of Testing_Refinements_by_Refining_Tests.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Language: English
Click to download this file (215kB) Preview
[thumbnail of]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


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.

Item Type: Book section
DOI/Identification number: 10.1007/978-3-540-49676-2_19
Additional information: 11th International Conference of Z Users on the Z Formal Specification Notation (ZUM 98) BERLIN, GERMANY, SEP 24-26, 1998 Daimler Benz AG; GMD FIRST; Tech Univ Berlin; Praxis Crit Syst
Uncontrolled keywords: Formal Method, Surjective Function, Disjunctive Normal Form, Generate Test Case, Partition Analysis
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Eerke Boiten
Date Deposited: 26 Jun 2009 10:00 UTC
Last Modified: 16 Nov 2021 09:55 UTC
Resource URI: (The current URI for this page, for reference purposes)
Boiten, Eerke Albert:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.