Abstract
In this paper we introduce an algorithm to automatically encode an ASM specification in PROMELA, the language of the model checker Spin, and we present a method exploitingthe counter example generation feature of Spin, to automatically generate from ASM specifications test sequences which accomplish a desired coverage. ASMs are used as test oracles to predict the expected outputs of units under test. A prototype tool that implements the proposed method is also presented. Experimental results in evaluatingthe method are reported. The experiments include test sequence generation, tests execution, code coverage measurement for a case study implemented in Java, and comparison with random tests generation. Benefits and limitations in using model checkingare discussed.
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
Paul Ammann, Paul Black, and William Majursk. Usingmo del checking to generate tests from specifications. In Proceedings of 2nd IEEE International Conference on Formal Engineering Methods (ICFEM’98), Brisbane, Australia, December 1998. 276
Ramesh Bharadwaj and Constance L. Heitmeyer. Model checkingcom plete requirements specifications usingab straction. Automated Software Engineering, 6(1):37–68, January 1999. 276
Giuseppe Del Castillo and Kirsten Winter. Model checkingsu pport for the ASM high-level language. In Tools and Algorithms for Construction and Analysis of Systems, pages 331–346, 2000. 267
P.-J. Courtois and David L. Parnas. Documentation for safety critical software. In Proc. 15th Int’l Conf. on Softw. Eng. (ICSE’ 93), pages 315–323, Baltimore, MD, 1993. 264, 268, 273
André Engels, Loe Feijs, and Sjouke Mauw. Test generation for intelligent networks usingmo del checking. In E. Brinksma, editor, TACAS’97, Lecture Notes in Computer Science 1217, pages 384–398. Springer, 1997. 275
Angelo Gargantini and Constance Heitmeyer. Using model checking to generate tests from requirements specifications. In Oscar Nierstrasz and Michel Lemoine, editors, Proceedings of the 7th European Engineering Conference and the 7th ACM SIGSOFT Symposium on the Foundations of Software Engeneering, volume 1687 of LNCS, sep 1999. 276
Angelo Gargantini and Elvinia Riccobene. Asm-based testing: Coverage criteria and automatic test sequence generation. Journal of Universal Computer Science, 7(11), 2001. 263, 269, 270, 273
Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, and Margus Veanes. Conformance testing with abstract state machines. Technical Report MSR-TR-2001-97, Microsoft Reasearch, October2001. 264, 275, 276
R. Hierons and J. Derrick. Special issue on specification-based testing. Software testing, verification & reliability (STVR), 10(4):201–262, December 2000. 263
G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–295, May 1997. 264
A. Jefferson Offutt, Yiwei Xiong, and Shaoying Liu. Criteria for generating specification-based tests. In Fifth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS’ 99), pages 119–131, 1999. 269
D. J. Richardson, S. L. Aha, and T.O. O’Malley. Specification-based test oracles for reactive systems. In Proceedings of the 14th International Conference onSoftware Engineering, pages 105–118. Springer, May 1992. 263
J. Schmid. Compilingab stract state machines to C++. Journal of Universal Computer Science, 7(11), 2001. 265
J. Schmid. Introduction to AsmGofer, 2001. 272
Gregory Tassey. The economic impacts inadequateinfrastructure software testing. Technical Report Planning Report 02-3, National Institute ofStandards andTechnology, May 2002. 263
Elaine J. Weyuker. Translatability and decidability questions for restricted classes of program schemas. SIAM Journal on Computing, 8(4):587–598, 1979. 271
Hong Zhu, Patrick A.V. Hall, and John H.R. May. Software unit text coverage and adequacy. ACM Computing Surveys, 29(4):366–427, December 1997. 263, 271
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
Gargantini, A., Riccobene, E., Rinzivillo, S. (2003). Using Spin to Generate Tests from ASM Specifications. 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_15
Download citation
DOI: https://doi.org/10.1007/3-540-36498-6_15
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