Marie-Claude Gaudel

Formal specifications and software testing: a fruitful convergence.

This talk will report the history of ideas and the main advances in the domain of software testing based on formal specifications. Going back to the seventies, being a bit caricatural, software testing was perceived, on the one hand, by its actors as an empirical activity that had nothing to gain from formal methods, on the other hand, by the advocates of these methods as doomed to disappear since in the long run programs will be correct by construction… At the date of this workshop, these two communities do not yet reach a complete consensus. But fortunately there have been some significant moves from both sides and various success stories that allow saying that there is a fruitful convergence toward testing methods based on formal specifications. Sound and effective testing methods have been established based on various types of formal specifications, leading to tools for assisting the testing process. A comprehensive survey can be found in [Hierons et al. 2009].

In the seventies and before, most works in the area were based on finite state machines, an approach inspired by circuit testing, then applied to software [Chow 78] and later on widely developed and extended for conformance testing of communication protocols, as surveyed in [Lee and Yannakakis 1996]. A notable exception is the foundational paper by Goodenough and Gerhart in 1975 where the importance of “all the conditions relevant to the correct operation of a program”, namely its logical specification, was pointed out, and the derivation of test cases from such specifications, was introduced.

This approach developed slowly during the eighties for various kinds of formal specification languages [Gannon McMullin 81], [Jalote 83], [Bougé et al. 86], [Hall 88], [Brinksma 88] despite the recurrent questions on the interest of testing pieces of software that have been formally specified and proved correct w.r.t. their specifications.

In the nineties, however, several well founded methods often validated by prototypical tools and convincing case studies provided evidence of the interest of the approach. One can mention (among many others) [Bernot Gaudel Marre 1991] and [Gaudel 1995] for algebraic specifications, [Dick Faivre 1993] for VDM, [Carrington Stocks 1994] for VDM, etc. This led to important research projects resulting in exploitable testing environments such as TGV, BZ, Asm, Z (SANTEN 97, Hierons 97), TorX, GATEL, etc. Since the beginning of the 21th century such tools and methods have greatly benefited of advances in the areas of constraint solvers [de Moura Bjorner 2008], symbolic evaluation [Cadar et al.], theorem provers [Brucker Wolff 2012], and of the increasing acceptance of formal methods in industrial projects.

References

1. R. M. Hierons, K. Bogdanov, J. P. Bowen, R. Cleaveland, J. Derrick, J. Dick, M. Gheorghe, M. Harman, K. Kapoor, P. Krause, G. Luttgen, A. J. H. Simons, S. Vilkomir, M. R. Woodward, and H. Zedan, Using formal specifications to support testing, ACM Comput. Surv. 41(2), 1-76, 2009.
2. T. Chow, Testing software design modeled by finite-state machines, IEEE Trans. on Software Engineering, SE-4(3):178187, 1978.
3. D. Lee and M. Yannakakis, Principles and methods of testing finite state machines—a survey, Proceedings of the IEEE, 84(8):1090-1123, 1996.
4. J. B. Goodenough and S. L. Gerhart, Toward a theory of test data selection, IEEE Trans. on Software Engineering, SE-1(2): 156-173, 1975.
5. J. Gannon, P. McMullin and R. Hamlet, Data Abstraction, Implementation, Specification, and Testing, ACM Trans. Program. Lang. Syst.,3(3):211-223, 1981.
6. P. Jalote, Specification and Testing of Abstract Data Types, COMSAC83, pp. 508- 511, 1983.
7. L. Bougé and N. Choquet and L. Fribourg and M.-C. Gaudel, Test set generation from algebraic specifications using logic programming, Journal of Systems and Software, 6(4): 343-360, 1986.
8. P.A.V. Hall, Towards testing with respect to formal specification, Second IEE/BCS Conference: Software Engineering, pp.159 - 163, 1988.
9. E. Brinksma, A theory for the derivation of tests, in: Protocol Specification, Testing, and Verification, VIII, North-Holland, 1988, pp. 63-74.
10. 10. G. Bernot, M.-C. Gaudel, and B. Marre, Software testing based on formal specifications: a theory and a tool, Soft. Eng. Journal, 6(6):387-405, 1991.
11. Gaudel, M.-C., Testing can be formal, too, TAPSOFT’95, LNCS 915, pp. 82-96, 1995.
12. J. Dick and A. Faivre, Automating the generation and sequencing of test cases from model-based specifications, LNCS 670, pp. 268-284, 1993.
13. Ph. Stocks, D.A. Carrington, Test Templates: A Specification-Based Testing Framework. ICSE 1993: 405-414
14. E. Brinksma and J. Tretmans, Testing Transition Systems: An Annotated Bibliography, LNCS 2076, 187-195, 2001.
15. L. De Moura and N. Bjørner. Z3: An efficient SMT solver, LNCS 4963, 337-340, 2008.
16. C. Cadar, P. Godefroid, S. Khurshid, C. S. Pasareanu, K. Sen, N.Tillmann, and W. Visser, Symbolic execution for software testing in practice: preliminary assessment, ICSE ’11, 1066-1071, 2011.
17. A. D. Brucker and B. Wolff, On Theorem Prover-based Testing, Formal Aspects of Computing, 25(5):683-721, 2013.