Techniques for Automated Test Generation from System Specifications

This paper discusses an approach to the practical exploitation of system specifications as a basis for generating tests.

Testing is seen as a means of increasing the confidence that a software product accurately realizes customer requirements. In safety-critical systems, the level of assurance required is particularly stringent. Yet, although proof of correctness is seen as one means of attaining this, testing is still of importance, especially where COTS components and standard operating systems are used. The high costs associated with testing take their toll on project budgets. Consequently, the automatic generation of test cases and the generation of tests from system specifications have become areas of interest.

Specification-based testing [7] aims to exploit the system specification in order to generate suitable tests for the implementation. Confidence into the correctness will be gained from successful tests.

A number of problems must be faced in automatic test generation from system specifications:

• Suitable framework. The selection of the framework within the tests will be generated plays a vital role in the success of the automation attempt. Some frameworks do not cater for developer needs as the expressiveness is limited, others are unsuitable for automation&nbsp[5]. Other problems are specific to the underlying theory or chosen approach and vary much, see e.g. [4] or [3].
• Test selection. There may be an infinitely large space of tests from which a choice must be made. This makes automation difficult and calls for additional assumptions that may not be satisfied in the given context. In order to make test selection viable, a test strategy, which defines the relevance of tests, must be proposed. Test strategies are developed for company wide use or can be specific to an application domain. Some testing methods impose a selection strategy on the user. Testers are very reluctant to adopt other strategies mainly because they have a strong believe into those which where developed for their needs.
• Abstract vs. Concrete Tests. The problems caused by abstraction depend on the proposed formalism of the specification. If the specification language is close to the implementation, then the benefits from the specification are limited. If the specification is more abstract, then the relation between generated tests and implementation becomes more loose. It is important to have the possibility of abstract representation with a close link to the implementation.

All of these problems tend to lead to stronger assumptions and less rigorous testing.

We propose to address those problems by using a special form of algebraic specifications [8], customised for developer needs. This approach is based on previous work by Bougé et.al. [1] and continued work by Gaudel and Marre [2, 6]. From a given specification we use a term rewriting system to generate abstract tests in the form of terms of the specification. A test strategy selects the appropriate tests which are transformed into concrete tests on the implementation using a reverse parsing technique to bridge the gap between abstract specification and actual software system. These generated tests are applied to the implementation and the outcome is observed.

• Automation. The initiality of algebraic specification models gives us the guarantee that we can produce test cases automatically, because it ensures the existence of terms for each possible value.
• Finite Test Space. The operations described in the specification may be split into generators and non-generators. The formalism also provides the possibility of recording restrictions on the input domains of operations. Large but finite test sets can be constructed from variable-free generator terms with restrictions on some sorts.
• Test selection. Relevant tests are selected by means of a test strategy. Here we propose to use common strategies already employed by testers, who are best equipped to judge which technique is effective under the given circumstances. Given a strategy, selection uses a partial order defined on terms built from generators.
• Transformation of Abstract Tests. Given the abstract tests the approach then uses a part of the specification expressed by means of a grammar to produce tests in the concrete representation so that they can we applied to the implementation.

The approach is illustrated in Figure 1.

The main goal of current work is that all these steps can be performed automatically with minimal user interference. Meanwhile we do not need to change the underlying theory for any step of the generation process. That gives us the advantage to be able to prove that selected tests are logical consequences of a specification and thereby gain confidence into the correctness of the implementation.

The approach is currently being investigated through an industrial sized pilot study adapted from that of Mayrhauser and Mraz [9] generating tests for an automated cartridge storage system, the StorageTek 4400.

References

[1] G. Bernot, M. C. Gaudel, and B. Marre. "A formal approach to software testing." In Proceedings of the Second International Conference on Algebraic Methodology and Software Technology, pages 163--170, Iowa City, Iowa, May 1991. The University of Iowa, Department of Computer Science.

[2] L. Bougé, N. Choquet, L. Fribourg, and M.-C. Gaudel. "Test sets generation from algebraic specifications using logic programming." Journal of Systems and Software, 6(4):343--360, 1986.

[3] D. Carrington and P. Stocks. "A tale of two paradigms: Formal methods and software testing." In J. P. Bowen and J. A. Hall, editors, Z User Workshop, Cambridge 1994, Workshops in Computing, pages 51--68. Springer-Verlag, 1994.

[4] J. Dick and A. Faivre. "Automating the generation and sequencing of test cases from model-based specifications." In J. C. P. Woodcock and P. G. Larsen, editors, FME'93: Industrial-Strength Formal Methods, pages 268--284. Formal Methods Europe, Springer-Verlag, Apr. 1993. Lecture Notes in Computer Science 670.

[5] M. R. Donat. "Automating formal specification-based testing." In M. Bidoit and M. Dauchet, editors, TAPSOFT '97:Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, volume 1214 of Lecture Notes in Computer Science, pages 833--847. Springer-Verlag, Apr. 1997.

[6] M.-C. Gaudel. "Testing can be formal, too." Lecture Notes in Computer Science, 915:82--96, 1995.

[7] R. M. Poston. Automating Specification-Based Software Testing. IEEE Computer Society Press, 1996.

[8] H. Reichel. Initial Computability, Algebraic Specifications, and Partial Algebras. Oxford University Press, 1987.

[9] A. von Mayrhauser, J. Walls, and R. Mraz. "Sleuth: A domain-based testing tool." In International Test Conference, pages 840--849, Altoona, Pa., USA, Oct. 1994. IEEE Computer Society Press.

1. Authors contact: Centre for Software Reliability, University of Newcastle upon Tyne.,
Newcastle, NE1 7RU, England. Phone: +44 191 222 7999. Fax: +44 191 222 8788.
E-Mail: {Andrej.Pietschker,John.Fitzgerald}@ncl.ac.uk.