Abstract
Testing is one of the most important and most time-consuming tasks in the software developing process and thus techniques and systems to automatically generate and check test cases have become crucial. In previous work we have presented techniques to test membership equational logic specifications; these techniques consist of two steps: first several ground terms are generated by using all the available constructor symbols in a breadth-first search, and then these terms are processed to check whether they fulfill some properties. This approach presents the drawback of separating two related processes, thus examining several terms that are indistinguishable from the point of view of testing. We present here a narrowing-based test-case generator that improves the performance of the tool and extends its use to rewriting logic specifications. First, we present two mechanisms to improve the narrowing commands currently available in Maude to use conditional statements and equational modules. Then, we show how to use these new narrowing commands to perform three different approaches to testing for any Maude specification: code coverage, property-based testing, and conformance testing. Finally, we present trusting mechanisms to improve the performance of the tool. We illustrate the tool by means of an example.
Research supported by MEC Spanish project DESAFIOS10 (TIN2009-14599-C03-01) and Comunidad de Madrid program PROMETIDOS (S2009/TIC1465).
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
Beizer, B.: Software testing techniques. Dreamtech (2002)
Borba, P., Cavalcanti, A., Sampaio, A., Woodcook, J. (eds.): PSSE 2007. LNCS, vol. 6153. Springer, Heidelberg (2010)
Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theoretical Computer Science 236, 35–132 (2000)
Brinksma, E., Scollo, G., Steenbergen, C.: LOTOS specifications, their implementations and their tests. In: Protocol Specification, Testing, and Verification VI, pp. 349–360 (1987)
Cartaxo, E.G., Neto, F.G.O., Machado, P.D.L.: Test case generation by means of UML sequence diagrams and labeled transition systems. In: Proceedings of the IEEE International Conference on Systems, Man and Cybernetics, SMC 2007, pp. 1292–1297. IEEE (2007)
Christiansen, J., Fischer, S.: EasyCheck — Test Data for Free. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, pp. 322–336. Springer, Heidelberg (2008)
Claessen, K., Hughes, J.: Quickcheck: A lightweight tool for random testing of Haskell programs. ACM SIGPLAN Notices, 268–279 (2000)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (Version 2.6) (January 2011), http://maude.cs.uiuc.edu/maude2-manual
Dupuy, A., Leveson, N.: An empirical evaluation of the MC/DC coverage criterion on the HETE-2 satellite software. In: Proceedings of the 19th Digital Avionics Systems Conference, DASC 2000, vol. 1, pp. 1B6.1–1B6.7 (2000)
Escobar, S., Meseguer, J.: Symbolic Model Checking of Infinite-State Systems Using Narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 153–168. Springer, Heidelberg (2007)
Fay, M.: First-order unification in an equational theory. In: Joyner, W.H. (ed.) Proceedings of the 4th Workshop on Automated Deduction, pp. 161–167. Academic Press (1979)
Fischer, S., Kuchen, H.: Systematic generation of glass-box test cases for functional logic programs. In: Proceedings of the 9th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, PPDP 2007, pp. 63–74. ACM Press (2007)
Gaudel, M.-C.: Software Testing Based on Formal Specification. In: Borba, P., Cavalcanti, A., Sampaio, A., Woodcook, J. (eds.) PSSE 2007. LNCS, vol. 6153, pp. 215–242. Springer, Heidelberg (2010)
Gomez-Zamalloa, M., Albert, E., Puebla, G.: Test case generation for object-oriented imperative languages in CLP. Theory and Practice of Logic Programming 10, 659–674 (2010)
Hussmann, H.: Unification in Conditional Equational Theories. In: Caviness, B.F. (ed.) EUROCAL 1985. LNCS, vol. 204, pp. 543–553. Springer, Heidelberg (1985)
Hierons, R.M., Bogdanov, K., Bowen, J.P., Rance Cleaveland, J.D., Dick, J., Gheorghe, M., Harman, M., Kapoor, K., Krause, P., Lüttgen, G., Simons, A.J.H., Vilkomir, S., Woodward, M.R., Zedan, H.: Using formal specifications to support testing. ACM Computing Surveys 41(2), 1–76 (2009)
Jacquemard, F., Rusinowitch, M., Vigneron, L.: Compiling and Verifying Security Protocols. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 131–160. Springer, Heidelberg (2000)
Jasper, R., Brennan, M., Williamson, K., Currier, B., Zimmerman, D.: Test data generation and feasible path analysis. In: Proceedings of the 1994 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 1994, pp. 95–107. ACM (1994)
King, J.C.: Symbolic execution and program testing. Communications of the ACM 19, 385–394 (1976)
Meadows, C.: Applying formal methods to the analysis of a key management protocol. Journal of Computer Security 1 (1992)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)
Middeldorp, A., Hamoen, E.: Counterexamples to Completeness Results for Basic Narrowing. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol. 632, pp. 244–258. Springer, Heidelberg (1992)
Müller, R.A., Lembeck, C., Kuchen, H.: A symbolic Java virtual machine for test case generation. In: IASTED Conf. on Software Engineering, pp. 365–371 (2004)
Ntafos, S.C.: A comparison of some structural testing strategies. IEEE Transactions on Software Engineering 14, 868–874 (1988)
Pacheco, C.: Directed Random Testing. PhD thesis, Massachusetts Institute of Technology (June 2009)
Riesco, A.: Test-Case Generation for Maude Functional Modules. In: Mossakowski, T., Kreowski, H.-J. (eds.) WADT 2010. LNCS, vol. 7137, pp. 287–301. Springer, Heidelberg (2012)
Riesco, A., Verdejo, A., Martí-Oliet, N., Caballero, R.: Declarative debugging of rewriting logic specifications. Journal of Logic and Algebraic Programming (2011) (to appear)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM 12(1), 23–41 (1965)
Runciman, C., Naylor, M., Lindblad, F.: Smallcheck and Lazy Smallcheck: automatic exhaustive testing for small values. In: Gill, A. (ed.) Proceedings of the 1st ACM SIGPLAN Symposium on Haskell, Haskell 2008, Victoria, BC, Canada, September 25, pp. 37–48. ACM (2008)
Slagle, J.R.: Automated theorem-proving for theories with simplifiers, commutativity and associativity. Journal of the ACM 21(4), 622–642 (1974)
Tretmans, J.: Model Based Testing with Labelled Transition Systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 1–38. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Riesco, A. (2012). Using Narrowing to Test Maude Specifications. In: Durán, F. (eds) Rewriting Logic and Its Applications. WRLA 2012. Lecture Notes in Computer Science, vol 7571. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34005-5_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-34005-5_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34004-8
Online ISBN: 978-3-642-34005-5
eBook Packages: Computer ScienceComputer Science (R0)