Testing Non-Deterministic State Machines with Fault Coverage
Susumu Fujiwara, Gregor von Bochmann · 1991
The selection of appropriate cases is an important issue in the development of communication protocols. Various case selection methods have been developed for the case that the protocol specification is given in the form of a deterministic finite state machine (FSM). This paper present a new method which applies in the case of nondeterministic specifications and implementations. The testing process is more complex if the specification, or even the implementation, is non-deterministic. Nevertheless, under appropriate assumptions, the described case selection method leads to a finite set of finite cases for a given specification which guarantees that any deviation of the implementation from the specification will be detected. The paper presents the new selection method in a framework for testing non-deterministic systems and demonstrates its use with small examples. 1. Introduction Testing plays an important role during the development of computer hardware and software. The selection of appropriate cases is an important issue in this context. We assume in this paper that a specification of the desired behavior of the system component to be tested is available. Such a specification can be taken as the basis for the development of a suite of cases, or for evaluating the coverage of a given suite. This paper deals with the development of a suite covering the behavior of a system component defined by a finite state machine specification. In contrast to most methods described in the literature, we allow for non-deterministic specifications and implementations. The issue of testing implementations in respect to a specified behavior has recently received much attention in the area of communication protocols [Rayn 87, Sari 89]. In order to validate the protocol implementation, a set of cases, usually called a test suite, is needed to determine whether an implementation conforms to its specification. In the case that a formal specification of the protocol is available, the selection and fault analysis can be based on this specification [Sari 89, Boch 89m]. This paper considers the case that the specification and its implementation may have nondeterministic behaviors. We assume that both the specification and the implementation can be modelled by finite labelled transition systems. In addition to finite state machines, there are many languages which are based on (in general infinite) labelled transition systems, such as CCS [Miln 80], CSP [Hoar 85], and LOTOS [Bolo 87]. The method described in this paper can be adapted to (subsets of) these languages. Most selection methods for (deterministic) finite state machines [Nait 81, Chow 78, Gone 70, Sabn 88] assume that the purpose of testing is to demonstrate that the behavior of