Specification for Testing - Formal Methods and Hybrid Real-Time Systems - page 280

Specification for Testing

Chris George 1 , Padmanabhan Krishnan 2 ,
P. A . P. S a l a s 2 , and J.W. Sanders 1

1

United Nations University International Institute for Software Technology, Macao
2

School of Information Technology, Bond University, Australia

Abstract. The success of model-based testing, in automating the testing of an
implementation given its state-based (or model-based) specification, raises the
question of how best the specification can be tweaked in order to facilitate that
process. This paper discusses several answers. Motivated by an example from
web-based systems, and taking account of the restriction imposed by the testing
interface, it considers both functional and non-functional properties. The former
include laws, implicit system invariants and other consistency conditions whilst
the latter include security leaks. It concludes that because of the importance of
the link between specification and implementation in the testing process, there is
a trade-off between genuinely useful testing information and the incorporation of
some degree of information about the link, not normally regarded as part of the
specification.

1 Introduction

(Formal) specifications and implementations are normally viewed as being poles apart.
After all, a specification captures requirements by expressing what a system should
achieve, whilst the purpose of an implementation is to be executed and so it contains
much detail whose concern is computational efficiency; the connection is of course that
the implementation conforms to the specification—ideally! They might also be viewed
as being poles apart because, after all, much of the process of system development lies
between a specification and an implementation.
Because that conformance is only ideal, testing is required. All testing presupposes
apriori , an oracle, knowledge for interpreting test outcomes: of which tests pass and
which fail. That knowledge constitutes, for any system of realistic size, only partial
information about the specification. But it demonstrates an unbreakable link between
specification and testing.
The advent of the important area of model-based testing, MBT, [7,9,26] forges an
even stronger link. Its primary importance is the complete automation of validation
testing, subject to control by the test engineer of those features of the system being
tested, of coverage criteria and so on. As pointed out by Utting [25], MBT relies on
redundancy between the test specification and the implementation; and then it is equally
likely to reveal errors in each.
Over the past couple of decades, considerable experience has been gained in specifi-
cation. The cost of the time spent on specification during the critical early stages of the
development cycle can be partly amortized over the later activity of testing using MBT.