Abstract
Software testing is typically an ad hoc process where human testers manually write many test inputs and expected test results, perhaps automating their execution in a regression suite. This process is cumbersome and costly. This paper reports preliminary results on an approach to further automate this process. The approach consists of combining automated test case generation based on systematically exploring the program’s input domain, with runtime analysis, where execution traces are monitored and verified against temporal logic specifications, or analyzed using advanced algorithms for detecting concurrency errors such as data races and deadlocks. The approach suggests to generate specifications dynamically per input instance rather than statically once-and-for-all. The paper describes experiments with variants of this approach in the context of two examples, a planetary rover controller and a space craft fault protection system.
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.
Similar content being viewed by others
References
S. Bensalem and K. Havelund. Reducing False Positives in Runtime Analysis of Deadlocks. Submitted for publication, October 2002. 91, 93, 95
C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated Testing Based on Java Predicates. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), July 2002. 90
G. Brat, D. Giannakopoulou, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, A. Venet, and W. Visser. A Comparative Field Study of Advanced Verification Technologies. Internal report, in preparation for submission, November 2002. 87, 95
M. Clavel, F. J. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. F. Quesada. Maude: Specification and Programming in Rewriting Logic, March 1999. Maude System documentation at maude.csl.sri.com/papers. 94
S. Cohen. Jtrek. Compaq, http://www.compaq.com/java/download/jtrek. 92
D. Drusinsky. The Temporal Rover and the ATG Rover. In SPIN Model Checking and Software Verification, volume 1885 of LNCS, pages 323–330. Springer, 2000. 89, 91, 93, 94
D. Drusinsky. Monitoring Temporal Rules with Temporal Data. Submitted for publication, October 2002. 94
M. Feather, S. Fickas, and N. Razermera-Mamy. Model-Checking for Validation of a Fault Protection System. In Proceedings of Sixth IEEE International Symposium on High Assurance System Engineering. IEEE Computer Society, October 2001. 103
E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns-Elements of Reusable Object-Oriented Software. Addison-Wesley, 1995. 92
W. Grieskamp, Y. Gurevich, W. Schulte, and M. Veanes. Generating Finite State Machines from Abstract State Machines. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), July 2002. 89
A. Groce and W. Visser. Model Checking Java Programs using Structural Heuristics. In Proceedings of the 2002 International Symposium on Software Testing and Analysis (ISSTA). ACM Press, July 2002. 90
A. Hartman. Model Based Test Generation Tools. http://www.agedis.de/documents/ModelBasedTestGenerationToolsc s.pdf+.89
K. Havelund, S. Johnson, and G. Roşu. Specification and Error Pattern Based Program Monitoring. In Proceedings of the European Space Agency workshop on On-Board Autonomy, Noordwijk, The Netherlands, October 2001. 95
K. Havelund and G. Roşu. Monitoring Java Programs with Java PathExplorer. In K. Havelund and G. Roşu, editors, Proceedings of the First International Workshop on Runtime Verification (RV’01), volume 55 of Electronic Notes in Theoretical Computer Science, pages 97–114, Paris, France, July 2001. Elsevier Science. 91, 93
K. Havelund and G. Roşu. Monitoring Programs using Rewriting. In Proceedings of the International Conference on Automated Software Engineering (ASE’01), pages 135–143. IEEE CS Press, 2001. Coronado Island, California. 95
K. Havelund and G. Roşu. A Rewriting-based Approach to Trace Analysis. Submitted for journal publication, September 2002. 95
K. Havelund and G. Roşu. Synthesizing Monitors for Safety Properties. In Tools and Algorithms for Construction and Analysis of Systems (TACAS’02), volume 2280 of Lecture Notes in Computer Science, pages 342–356. Springer, 2002. EASST best paper award at ETAPS’02. 95
H. Hong, I. Lee, O. Sokolsky, and H. Ural. A Temporal Logic Based Theory of Test Coverage and Generation. In Proceedings of the 8th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), April 2002. 90
J. C. King. Symbolic Execution and Program Testing. Communications of the ACM, 19(7):385–394, 1976. 89
B. Korel. Automated Software Test Data Generation. IEEE Transaction on Software Engineering, 16(8):870–879, August 1990. 89
Parasoft. http://www.parasoft.com. 89
A. Pnueli. The Temporal Logic of Programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pages 46–77, 1977. 93
S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: A Dynamic Data Race Detector for Multithreaded Programs. ACM Transactions on Computer Systems, 15(4):391–411, November 1997. 95
N. Tracey, J. Clark, and K. Mander. The Way Forward for Unifying Dynamic Test-Case Generation: The Optimisation-Based Approach. In International Workshop on Dependable Computing and Its Applications (DCIA), pages 169–180. IFIP, January 1998. 89
T-VEC. http://www.t-vec.com. 89
W. Visser, K. Havelund, G. Brat, and S. Park. Model Checking Programs. In Proceedings of ASE’2000: The 15th IEEE International Conference on Automated Software Engineering. IEEE CS Press, September 2000. 90
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Artho, C. et al. (2003). Experiments with Test Case Generation and Runtime Analysis. In: Börger, E., Gargantini, A., Riccobene, E. (eds) Abstract State Machines 2003. ASM 2003. Lecture Notes in Computer Science, vol 2589. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36498-6_5
Download citation
DOI: https://doi.org/10.1007/3-540-36498-6_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00624-4
Online ISBN: 978-3-540-36498-6
eBook Packages: Springer Book Archive