Gilbert Laycock, PhD Thesis Abstract: The Theory and
Practice of Specification Based Software Testing
This is the abstract to my PhD thesis:
- [Laycock92] Gilbert
- The Theory and Practice of Specification Based
Software Testing. Department of Computer Science,
University of Sheffield (1993).
In this thesis my aim is to examine the common ground between
formal methods and testing, and the benefits the two fields
bring to one another. All too often they are regarded as
mutually exclusive approaches in the development of software
The thesis begins with an examination of the motivation behind
software testing, a summary of its development over the past
few decades, and a survey of existing techniques. This
involves a detailed discussion of some of those techniques,
and leads on to an extensive case study.
The case study shows how the use of a formal specification
enables an existing "partition" based testing method to be
used with far greater precision, but also highlights some of
the limitations of the partition based techniques.
The thesis continues with a comprehensive look at the
development of theoretical models of testing since the mid
1970's, and the way they have used successively more complex
software models in order to be able to adequately describe
suitable test cases.
The remainder of the thesis is concerned with the introduction
and use of Eilenberg's X-machines as a formal model for the
description of software specifications. The goal is to develop
the X-machine model to the point where it is both useful and
use-able as a tool for system specification, and at the same
time the basis for a model of software testing so that test
cases can be derived directly from the specification. To this
end some of the theoretical properties of X-machines are
examined, and some simple but very relevant results
proved. The work is grounded on further case studies.
You can download the whole thesis
from here as PDF.