Skip to main content
SpringerLink
Log in

Using Semantics Specified in Maude to Generate Test Cases

  • Conference paper
Theoretical Aspects of Computing – ICTAC 2012 (ICTAC 2012)

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

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 generate and check test cases have become crucial. For these reasons, when specifying a prototype of a programming language it may be very useful to have a tool that, beyond testing the semantics of the program, generates test cases for the programs written in the specified language. In this way, we could use the test cases generated in the prototyping stage to check the implementation. To build these prototypes we can use rewriting logic, which has been proposed as a logical framework where other logics can be represented, and as a semantic framework for the specification of languages and systems.

In this paper we propose a technique to generate test cases for programs written in programming languages specified in Maude, although it can be generalized to similar languages. In this way Maude becomes an even more powerful prototyping language providing a test-case generator (in addition to an interpreter of the language). The test cases can be generated in two ways: computing a set of test cases using all the instructions required by a given coverage criterion or trying to disprove a property over the program. This methodology has been implemented in a Maude prototype and its use is described by means of an example.

Research supported by MICINN Spanish project DESAFIOS10 (TIN2009-14599-C03-01) and Comunidad de Madrid program PROMETIDOS (S2009/TIC-1465).

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 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 72.00
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. Beck, K., Gamma, E.: Test-infected: programmers love writing tests, pp. 357–376. Cambridge University Press (2000)

    Google Scholar 

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

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

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

    Google Scholar 

  5. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)

    MATH  Google Scholar 

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

  7. Ellison, C., Roşu, G.: An executable formal semantics of C with applications. In: Proceedings of the 39th Symposium on Principles of Programming Languages, POPL 2012, pp. 533–544. ACM (2012)

    Google Scholar 

  8. Fay, M.J.: 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 

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

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

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

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

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

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  15. Meseguer, J., Roşu, G.: The rewriting logic semantics project. Theoretical Computer Science 373(3), 213–237 (2007)

    Article  MathSciNet  MATH  Google Scholar 

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

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

  18. Papadakis, M., Sagonas, K.: A PropEr integration of types and function specifications with property-based testing. In: Proceedings of the 2011 ACM SIGPLAN Erlang Workshop, pp. 39–50. ACM Press (2011)

    Google Scholar 

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

  20. Riesco, A.: Using Narrowing to Test Maude Specifications. In: Durán, F. (ed.) Proceedings of the 9th International Workshop on Rewriting Logic and its Applications, WRLA 2012. LNCS. Springer (to appear, 2012)

    Google Scholar 

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

    Google Scholar 

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

  23. 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, pp. 37–48. ACM (2008)

    Google Scholar 

  24. Şerbănuţă, T., Ştefănescu, G., Roşu, G.: Defining and Executing P Systems with Structured Data in K. In: Corne, D.W., Frisco, P., Păun, G., Rozenberg, G., Salomaa, A. (eds.) WMC 2008. LNCS, vol. 5391, pp. 374–393. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

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

  26. Tretmans, J.: Conformance testing with labelled transition systems: Implementation relations and test generation. Computer Networks and ISDN Systems 29(1), 49–79 (1996)

    Article  Google Scholar 

  27. Verdejo, A., Martí-Oliet, N.: Executable structural operational semantics in Maude. Journal of Logic and Algebraic Programming 67, 226–293 (2006)

    Article  MathSciNet  MATH  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. National University of Singapore, Computing Drive 13, 117417, Singapore, Singapore

    Abhik Roychoudhury

  2. International Institute of Information Technology, Eletronics City 26-C, 560100, Bangalore, India

    Meenakshi D’Souza

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Riesco, A. (2012). Using Semantics Specified in Maude to Generate Test Cases. In: Roychoudhury, A., D’Souza, M. (eds) Theoretical Aspects of Computing – ICTAC 2012. ICTAC 2012. Lecture Notes in Computer Science, vol 7521. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32943-2_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-32943-2_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-32942-5

  • Online ISBN: 978-3-642-32943-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation