Skip to main content
SpringerLink
Log in

Using Narrowing to Test Maude Specifications

  • Conference paper
Rewriting Logic and Its Applications (WRLA 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7571))

Included in the following conference series:

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).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 49.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Beizer, B.: Software testing techniques. Dreamtech (2002)

    Google Scholar 

  2. Borba, P., Cavalcanti, A., Sampaio, A., Woodcook, J. (eds.): PSSE 2007. LNCS, vol. 6153. Springer, Heidelberg (2010)

    Google Scholar 

  3. Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theoretical Computer Science 236, 35–132 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  4. Brinksma, E., Scollo, G., Steenbergen, C.: LOTOS specifications, their implementations and their tests. In: Protocol Specification, Testing, and Verification VI, pp. 349–360 (1987)

    Google Scholar 

  5. 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)

    Google Scholar 

  6. 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)

    Chapter  Google Scholar 

  7. Claessen, K., Hughes, J.: Quickcheck: A lightweight tool for random testing of Haskell programs. ACM SIGPLAN Notices, 268–279 (2000)

    Google Scholar 

  8. 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)

    MATH  Google Scholar 

  9. 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

  10. 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)

    Google Scholar 

  11. 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)

    Chapter  Google Scholar 

  12. 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)

    Google Scholar 

  13. 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)

    Google Scholar 

  14. 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)

    Chapter  Google Scholar 

  15. 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)

    Article  MathSciNet  MATH  Google Scholar 

  16. Hussmann, H.: Unification in Conditional Equational Theories. In: Caviness, B.F. (ed.) EUROCAL 1985. LNCS, vol. 204, pp. 543–553. Springer, Heidelberg (1985)

    Google Scholar 

  17. 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)

    Article  Google Scholar 

  18. 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)

    Chapter  Google Scholar 

  19. 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)

    Google Scholar 

  20. King, J.C.: Symbolic execution and program testing. Communications of the ACM 19, 385–394 (1976)

    Article  MATH  Google Scholar 

  21. Meadows, C.: Applying formal methods to the analysis of a key management protocol. Journal of Computer Security 1 (1992)

    Google Scholar 

  22. Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  23. 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)

    Chapter  Google Scholar 

  24. 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)

    Google Scholar 

  25. Ntafos, S.C.: A comparison of some structural testing strategies. IEEE Transactions on Software Engineering 14, 868–874 (1988)

    Article  Google Scholar 

  26. Pacheco, C.: Directed Random Testing. PhD thesis, Massachusetts Institute of Technology (June 2009)

    Google Scholar 

  27. 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)

    Chapter  Google Scholar 

  28. Riesco, A., Verdejo, A., Martí-Oliet, N., Caballero, R.: Declarative debugging of rewriting logic specifications. Journal of Logic and Algebraic Programming (2011) (to appear)

    Google Scholar 

  29. Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM 12(1), 23–41 (1965)

    Article  MATH  Google Scholar 

  30. 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)

    Google Scholar 

  31. Slagle, J.R.: Automated theorem-proving for theories with simplifiers, commutativity and associativity. Journal of the ACM 21(4), 622–642 (1974)

    Article  MathSciNet  MATH  Google Scholar 

  32. 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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Facultad de Informática, Universidad Complutense de Madrid, Spain

    Adrián Riesco

Authors
  1. Adrián Riesco
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Departamento de Lenguajes y Ciencias de la Computacíon, E.T.S.I Informática, Universidad de Málaga, Boulevard Louis Pasteur, s/n, Campus de Teatinos, 29071, Málaga, Spain

    Franciso Durán

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation