There has been considerable theoretical and practical work on how to automatically and semi-automatically generate test cases from formal specifications, and how scheduling of these tests can be achieved. Different types of formalisms have developed different ways to do this, for example, there has been considerable research on testing specifications in the context of process algebras [112,59,40,39]. A number of techniques have also been developed for state-based languages, see for example [174,55,71,48,123,189].
The approach we focussed on in this chapter has its roots in the work of Dick and Faivre [71], who describe a means to automate test generation and sequencing from VDM specifications. This work has also been applied to Z specifications in [123,177], and to Object-Z specifications in [162]. In [123] Hörcher describes an application of this methodology to a portion of the Cabin Intercommunication Data System for the Airbus A330/340 aircraft. In [177] this methodology is combined with the classification tree method [102] and is used to test an adaptive control system. Tool support for the technique is described in [71] and [202], and has been applied to B by van Aertryck [202] and Behnia and Waeselynck [16].
The idea of testing an implementation using a retrieve relation was first raised in [71]. The problem was also discussed by Stocks [194] and Stepney [189]. Hörcher discusses the problem in more depth in [123], and comments that retrieve relations may be used in the production of test oracles.
The work in this chapter was first described in [65] and [62] by Derrick and Boiten. [62] considered the partition analysis of individual operations and includes proofs of Theorems 7.2.1and 7.2.2. [65] described how to calculate the concrete FSM from the abstract. Although the results here are described with reference to the construction of finite state machines similar to that described in [71], they are also applicable to other approaches, such as those described in [162,117].