Abstract
The course “Testing, Debugging, and Verification” is a non-traditional formal methods course that connects formal approaches to real-world development techniques in a novel way. A general theme in the course is that formalisation of specifications is the basis for debugging and test generation tools that go beyond what is possible with merely informal methods, and ultimately provides the opportunity of formal verification. Thereby, the course aims at integrating formal and informal methods as much as possible. The course is supposed to be accessible to participants without extensive mathematical training. We report about the design, implementation, and experiences with the course.
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
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: The B Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Axelsson, E., Björk, M., Sheeran, M.: Teaching hardware description and verification. In: International Conference on Microelectronics Systems Education, Anaheim, CA, USA, pp. 119–120. IEEE Computer Society, Los Alamitos (2005)
Baum, M.: Debugging by visualizing of symbolic execution. Master’s thesis, Department of Computer Science, Institute for Theoretical Computer Science (June 2007)
Beckert, B., Hähnle, R., Schmitt, P.: Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
Ben-Ari, M.: Principles of the Spin Model Checker. Springer, Heidelberg (2008)
Bjørner, D.: Software Engineering, vol. 3. Springer, Heidelberg (2006)
Bubel, R., Hähnle, R.: A Hoare-style calculus with explicit state updates. In: Instenes, Z. (ed.) Proc. Formal Methods in Computer Science Education (FORMED). ENTCS, pp. 49–60. Elsevier, Amsterdam (2008)
Cheon, Y., Leavens, G.T.: A simple and practical approach to unit testing: The JML and JUnit way. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 231–255. Springer, Heidelberg (2002)
Cok, D.R., Kiniry, J.: ESC/Java2: Uniting ESC/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108–128. Springer, Heidelberg (2005)
de Halleux, J., Tillmann, N.: Parameterized unit testing with Pex. In: Beckert, B., Hähnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 171–181. Springer, Heidelberg (2008)
Engel, C.: Verification based test case generation. Master’s thesis, Department of Computer Science, University of Karlsruhe (August 2006)
Engel, C., Hähnle, R.: Generating unit tests from formal proofs. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 169–188. Springer, Heidelberg (2007)
Guttag, J.V., Horning, J.J., Garland, S.J., Jones, K.D., Modet, A., Wing, J.M.: Larch: Languages and Tools for Formal Specification. Springer, New York (1993)
King, J.C.: A program verifier. PhD thesis, Carnegie-Mellon University (1969)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06y, Iowa State University, Department of Computer Science (2003) (revised, June 2004)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P.: JML Reference Manual (February 2007); Draft revision 1.200
Lewis, B.: Debugging backwards in time. In: Ronsse, M. (ed.) Proc. Fifth Int. Workshop on Automated and Algorithmic Debugging, AADEBUG (September 2003)
Meyer, B.: Applying “design by contract”. IEEE Computer 25(10), 40–51 (1992)
Rothe, M.: Assisting the understanding of program behavior by using symbolic execution. Master’s thesis, Department of Computer Science and Engineering (July 2008)
Sommerville, I.: Software Engineering, 8th edn. Addison-Wesley, Reading (2006)
Zeller, A.: Why Programs Fail: A Guide to Systematic Debugging. Morgan Kaufmann, San Francisco (2005)
Zeller, A., Hildebrandt, R.: Simplifying and isolating failure-inducing input. IEEE Transactions on Software Engineering 28 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ahrendt, W., Bubel, R., Hähnle, R. (2009). Integrated and Tool-Supported Teaching of Testing, Debugging, and Verification. In: Gibbons, J., Oliveira, J.N. (eds) Teaching Formal Methods. TFM 2009. Lecture Notes in Computer Science, vol 5846. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04912-5_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-04912-5_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04911-8
Online ISBN: 978-3-642-04912-5
eBook Packages: Computer ScienceComputer Science (R0)