Skip to main content
SpringerLink
Log in

Incrementally Discovering Testable Specifications from Program Executions

  • Conference paper
Formal Methods for Components and Objects (FMCO 2009)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6286))

Included in the following conference series:

Abstract

The ProTest project is an EU FP7 project to develop techniques that improve the testing and verification of concurrent and distributed software systems. One of the four main work packages is concerned with the automated identification of specifications that could serve as a suitable basis for testing; this is currently a tedious and error-prone manual task that tends to be neglected in practice. This paper describes how this problem has been addressed in the ProTest project. It describes a technique that uses test executions to refine the specification from which they are generated. It shows how the technique has been implemented and applied to real Erlang systems. It also describes in detail the major challenges that remain to be addressed in future work.

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 54.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. Derrick, J., Walkinshaw, N.: Property-based testing: The protest project. In: FMCO (2009)

    Google Scholar 

  2. Armstrong, J.: Programming Erlang: Software for a Concurrent World. Pragmatic Bookshelf (July 2007)

    Google Scholar 

  3. Walkinshaw, N., Derrick, J., Guo, Q.: Iterative refinement of reverse-engineered models by model-based testing. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 305–320. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  4. Walkinshaw, N., Bogdanov, K., Holcombe, M., Salahuddin, S.: Improving Dynamic Software Analysis by Applying Grammar Inference Principles. Journal of Software Maintenance and Evolution: Research and Practice (2008)

    Google Scholar 

  5. Claessen, K., Hughes, J.: Quickcheck: A Lightweight Tool for Random Testing of Haskell Programs. In: Proceedings of the International Conference on Functional Programming (ICFP), pp. 268–279 (2000)

    Google Scholar 

  6. Walkinshaw, N., Bogdanov, K., Ali, S., Holcombe, M.: Automated discovery of state transitions and their functions in source code. Software Testing, Verification and Reliability 18(2) (2008)

    Google Scholar 

  7. Moore, E.F.: Gedanken–experiments on sequential machines. In: Shannon, C.E., McCarthy, J. (eds.) Annals of Mathematics Studies (34), Automata Studies, pp. 129–153. Princeton University Press, Princeton (1956)

    Google Scholar 

  8. Nerode, A.: Linear automata transformations. Proceedings of the American Mathematical Society 9, 541–544 (1958)

    Article  MathSciNet  MATH  Google Scholar 

  9. Gold, E.: Language Identification in the Limit. Information and Control 10, 447–474 (1967)

    Article  MathSciNet  MATH  Google Scholar 

  10. Biermann, A., Feldman, J.: On the Synthesis of Finite-State Machines from Samples of their Behavior. IEEE Transactions on Computers 21, 592–597 (1972)

    Article  MathSciNet  MATH  Google Scholar 

  11. Dupont, P., Lambeau, B., Damas, C., van Lamsweerde, A.: The QSM Algorithm and its Application to Software Behavior Model Induction. Applied Artificial Intelligence 22, 77–115 (2008)

    Article  Google Scholar 

  12. Walkinshaw, N., Bogdanov, K., Holcombe, M., Salahuddin, S.: Reverse Engineering State Machines by Interactive Grammar Inference. In: 14th IEEE International Working Conference on Reverse Engineering, WCRE (2007)

    Google Scholar 

  13. Cook, J., Wolf, A.: Discovering Models of Software Processes from Event-Based Data. ACM Transactions on Software Engineering and Methodology 7(3), 215–249 (1998)

    Article  Google Scholar 

  14. Ammons, G., Bodík, R., Larus, J.: Mining Specifications. In: 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Portland, Oregon, pp. 4–16 (2002)

    Google Scholar 

  15. Angluin, D.: Learning Regular Sets from Queries and Counterexamples. Information and Computation 75, 87–106 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  16. Shahbaz, M., Groz, R.: Inferring mealy machines. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 207–222. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  17. Lang, K., Pearlmutter, B., Price, R.: Results of the Abbadingo One DFA Learning Competition and a New Evidence-Driven State Merging Algorithm. In: Honavar, V.G., Slutzki, G. (eds.) ICGI 1998. LNCS (LNAI), vol. 1433, pp. 1–12. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  18. Biermann, A.W., Krishnaswamy, R.: Constructing programs from example computations. IEEE Trans. on Software Engineering SE 2, 141–153 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  19. Cicchello, O., Kremer, S.: Inducing grammars from sparse data sets: A survey of algorithms and results. Journal of Machine Learning Research 4, 603–632 (2003)

    MathSciNet  MATH  Google Scholar 

  20. Cheng, K., Krishnakumar, A.: Automatic functional test generation using the extended finite state machine model. In: 30th ACM/IEEE Design Automation Conference, pp. 86–91 (1993)

    Google Scholar 

  21. Walkinshaw, N., Bogdanov, K.: Inferring Finite-State Models with Temporal Constraints. In: Proceedings of the 23rd International Conference on Automated Software Engineering, ASE (2008)

    Google Scholar 

  22. Paris, J., Arts, T.: Automatic testing of tcp/ip implementations using quickcheck. In: Proceedings of the 8th ACM SIGPLAN workshop on Erlang, Erlang 2009, pp. 83–92. ACM, New York (2009)

    Google Scholar 

  23. Postel, J.: Transmission control protocol. Technical Report 793, DDN Network Information Center, SRI International, RFC (September 1981)

    Google Scholar 

  24. Ostrand, T., Balcer, M.: The category-partition method for specifying and generating functional tests. Communications of the ACM 31(6), 676–686 (1988)

    Article  Google Scholar 

  25. Damas, C., Lambeau, B., Dupont, P., van Lamsweerde, A.: Generating Annotated Behavior Models from End-User Scenarios. IEEE Transactions on Software Engineering 31(12), 1056–1073 (2005)

    Article  Google Scholar 

  26. Lorenzoli, D., Mariani, L., Pezzè, M.: Automatic generation of software behavioral models. In: Proceedings of the 30th international conference on Software engineering, ICSE 2008, pp. 501–510. ACM, New York (2008)

    Google Scholar 

  27. Ernst, M., Cockrell, J., Griswold, W., Notkin, D.: Dynamically Discovering Likely Program Invariants to Support Program Evolution. Transactions on Software Engineering 27(2), 1–25 (2001)

    Article  Google Scholar 

  28. Bongard, J.C., Lipson, H.: Nonlinear system identification using coevolution of models and tests. IEEE Trans. Evolutionary Computation 9(4), 361–384 (2005)

    Article  MATH  Google Scholar 

  29. Cornelissen, B., Zaidman, A., Holten, D., Moonen, L., van Deursen, A., van Wijk, J.: Execution trace analysis through massive sequence and circular bundle views. Journal of Systems and Software 81(12), 2252–2268 (2008)

    Article  Google Scholar 

  30. Afshan, S., McMinn, P., Walkinshaw, N.: Using dictionary compression algorithms to identify phases in program traces. Technical Report CS-10-01, Department of Computer Science, The University of Sheffield (2010)

    Google Scholar 

  31. Walkinshaw, N., Afshan, S., McMinn, P.: Using compression algorithms to support the comprehension of program traces. In: Proceedings of the Eighth International Workshop on Dynamic Analysis (WODA 2010). ACM, New York (2010)

    Google Scholar 

  32. Nevill-Manning, C., Witten, I.: Compression and explanation using hierarchical grammars. Computer Journal 40(2/3), 103–116 (1997)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, The University of Sheffield, Sheffield, UK

    Neil Walkinshaw & John Derrick

Authors
  1. Neil Walkinshaw
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. John Derrick
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Centre for Mathematics and Computer Science, CWI, Science Park 123, 1098, Amsterdam, XG, The Netherlands

    Frank S. de Boer

  2. Leiden Institute of Advanced Computer Science, Leiden University, P.O. Box 9512, 2300, Leiden, RA, The Netherlands

    Marcello M. Bonsangue

  3. Heinrich-Heine University of Dusseldorf, Dusseldorf, Germany

    Stefan Hallerstede

  4. Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, Universitätsstraße 1, 40225, Düsseldorf, Germany

    Michael Leuschel

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Walkinshaw, N., Derrick, J. (2010). Incrementally Discovering Testable Specifications from Program Executions. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds) Formal Methods for Components and Objects. FMCO 2009. Lecture Notes in Computer Science, vol 6286. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17071-3_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-17071-3_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-17070-6

  • Online ISBN: 978-3-642-17071-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation