Abstract
In this chapter, we apply Formal Methods to software and systems testing. After some introductory remarks on the importance of software testing in general, and formal rigour in particular, we give a typical example of a computational system as it occurs as part of a bigger system. We show how to formally specify and model such a system, how to define test cases for it, and how to monitor testing results with temporal logic. In order to do so, we use simplified state machines from the unified modelling language UML2. With the example, we describe the underlying methodology of test generation and discuss automated test generation methods and test coverage criteria. We present Tretmans’ classical conformance testing theory, and Gaudel’s theory of test generation from algebraic specifications. Finally, we discuss available tools, and point to research topics in the area of specification-based testing.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Change history
20 December 2022
.
Notes
- 1.
Here, we deviate from some parts of the literature where the words ‘error’ and ‘fault’ are interchanged; for us, an error (occurring in the human mind) is more fundamental than a fault (occurring in an artefact).
- 2.
Note that the use of the word ‘model’ significantly differs here from its use in logic. In MBD/MBT, a model is defined to be a purposeful abstraction of some target system, whereas in logic a model is a semantical structure for the evaluation of formulae.
- 3.
This fact has been used in the past by some car manufacturers to illegally program different behaviour for the carburettor when the car is under test or on the road.
- 4.
Note that this convention differs slightly from the use of the terms in logic, where a calculus is called sound if all provable statements are true, and complete if all true statements are provable.
References
Samson Abramsky. Observation equivalence as a testing equivalence. Theor. Comput. Sci., 53:225–241, 1987.
Larry Apfelbaum and John Doyle. Model based testing. In Software Quality Week Conference, May, 1997.
Paul Ammann and Jeff Offutt. Introduction to Software Testing. Cambridge University Press, 2008.
Boris Beizer. Software Testing Techniques. Van Nostrand Reinhold, 1990.
Gilles Bernot, Marie Claude Gaudel, and Bruno Marre. Software testing based on formal specifications: A theory and a tool. Softw. Eng. J., 6(6):387–405, November 1991.
Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, and Alexander Pretschner. Model-Based Testing of Reactive Systems: Advanced Lectures. Springer, 2005.
Igor B. Bourdonov, Alexander S. Kossatchev, Victor V. Kuliamin, and Alexander K. Petrenko. UniTesK test suite architecture. In FME 2002, LNCS 2391, pages 77–88. Springer, 2002.
Ed Brinksma and Jan Tretmans. Testing transition systems: An annotated bibliography. In MOVEP, LNCS 2067, pages 187–195. Springer, 2000.
Rance Cleaveland and Matthew Hennessy. Testing equivalence as a bisimulation equivalence. Formal Aspects of Computing, 5(1):1–20, Jan 1993.
Ana Cavalcanti and Robert M. Hierons. Testing with inputs and outputs in CSP. In FASE 2013, LNCS 7793, pages 359–374. Springer, 2013.
Edsger W. Dijkstra. Structured programming. In Software Engineering Techniques, 1970.
R. de Nicola and M. C. B. Hennessy. Testing equivalences for processes. In Automata, Languages and Programming, pages 548–560. Springer, 1983.
Adenilso da Silva Simão and Alexandre Petrenko. Generating complete and finite test suite for ioco: Is it possible? In MBT, volume 141 of EPTCS, pages 56–70, 2014.
William R. Elmendorf. Evaluation of the functional testing of control programs, 1967.
Marie-Claude Gaudel. Testing can be formal, too. In TAPSOFT ’95, pages 82–96, Berlin, Heidelberg, 1995. Springer.
Matthias Grochtmann and Klaus Grimm. Classification trees for partition testing. Softw. Test., Verif. Reliab., 3(2):63–82, 1993.
Yuri Gurevich and Bertrand Meyer, editors. Tests and Proofs, LNCS 4454. Springer, 2007.
Dorothy Graham, Erik Van Veenendaal, Isabel Evans, and Rex Black. Foundations of Software Testing: ISTQB Certification. Thomson, 2008.
William C. Hetzel, editor. Program test methods. Prentice-Hall, 1973.
Klaus Havelund and Grigore Rosu. Monitoring programs using rewriting. In ASE 2001, pages 135–143. IEEE, 2001.
Antti Huima. Implementing Conformiq Qtronic. In Testing of Software and Communicating Systems, pages 1–12. Springer, 2007.
Paul C. Jorgensen. Software Testing: A Craftsman’s Approach. CRC Press, 1st edition, 1995.
J.M. Juran. Quality-control handbook. McGraw-Hill, 1951.
Anne Kramer and Bruno Legeard. Model-Based Testing Essentials - Guide to the ISTQB Certified Model-Based Tester: Foundation Level. Wiley Publishing, 1st edition, 2016.
H.D. Leeds and G.M. Weinberg. Computer programming fundamentals. McGraw-Hill, 1961.
Aditya P. Mathur. Foundations of Software Testing. Addison-Wesley, 1st edition, 2008.
Curtis McEnroe. A formula for the number of days in each month, Friday, 5 December, 2014. https://cmcenroe.me/2014/12/05/days-in-month-formula.html.
Joris Meerts and Dorothy Graham. The history of software testing. http://www.testingreferences.com/testinghistory.php.
Glenford J. Myers. Art of Software Testing. Wiley, 1979.
OMG, Object Management Group. UTP, UML Testing Profile, v. 1.2, 2013.
Jan Peleska. Industrial-strength model-based testing - state of the art and current challenges. In MBT, volume 111 of EPTCS, pages 3–28, 2013.
Nikolay V. Pakulin, Alexander K. Petrenko, and Bernd-Holger Schlingloff, editors. MBT 2015, EPTCS 180, 2015.
Michael O. Rabin and Dana Scott. Finite automata and their decision problems. IBM J. Res. Dev., 3(2):114–125, April 1959.
Jan Tretmans. A formal approach to conformance testing. In Protocol Test Systems, volume C-19 of IFIP Transactions, pages 257–276. North-Holland, 1993.
Jan Tretmans. Test generation with inputs, outputs, and quiescence. In TACAS, LNCS 1055, pages 127–146. Springer, 1996.
Jan Tretmans. Model based testing with labelled transition systems. In Formal Methods and Testing, pages 1–38. Springer, 2008.
Mark Utting and Bruno Legeard. Practical Model-Based Testing: A Tools Approach. Morgan Kaufmann, 2007.
Stephan Weißleder and Bernd-Holger Schlingloff. Automatic model-based test generation from uml state machines. In Model-Based Testing for Embedded Systems. CRC Press, 2011.
Justyna Zander, Ina Schieferdecker, and Pieter Mosterman, editors. Model-Based Testing for Embedded Systems. CRC Press, 2011.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2022 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Schlingloff, BH., Roggenbach, M. (2022). Specification-Based Testing. In: Formal Methods for Software Engineering. Texts in Theoretical Computer Science. An EATCS Series. Springer, Cham. https://doi.org/10.1007/978-3-030-38800-3_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-38800-3_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-38799-0
Online ISBN: 978-3-030-38800-3
eBook Packages: Computer ScienceComputer Science (R0)