Towards a Tool Environment for Model-Based Testing with AsmL

  • Mike Barnett
  • Wolfgang Grieskamp
  • Lev Nachmanson
  • Wolfram Schulte
  • Nikolai Tillmann
  • Margus Veanes
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2931)


We present work on a tool environment for model-based testing with the Abstract State Machine Language (AsmL). Our environment supports semi-automatic parameter generation, call sequence generation and conformance testing. We outline the usage of the environment by an example, discuss its underlying technologies, and report on some applications conducted in the Microsoft environment.


Model Check Label Transition System Conformance Testing Abstract State Machine Shopping Cart 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Gurevrich, Y.: Evolving Algebras 1993: Lipari Guide. In: Boerger, E. (ed.) Specification and Validation Methods, pp. 9–36. Oxford University Press, Oxford (1995)Google Scholar
  2. 2.
    F.o.S. Engineering: The AsmL Release, Microsoft Research, Redmond (2000–2003)Google Scholar
  3. 3.
    Barnett, M., Schulte, W.: Runtime Verification of .NET Contracts. The Journal of Systems and Software, 199–208 (2002)Google Scholar
  4. 4.
    Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines - a survey. Proceedings of the IEEE 84, 1090–1123 (1996)CrossRefGoogle Scholar
  5. 5.
    Grieskamp, W., Gurevich, Y., Schulte, W., Veanes, M.: Generating Finite State Machines from Abstract State Machines. In: Proceedings of International Symposium on Software Testing and Analysis (ISSTA 2002), pp. 112–122. IEEE, Rome (2002)CrossRefGoogle Scholar
  6. 6.
    Mehlhorn, K., Schaefer, G.: A Heuristic for Dijkstra’s Algorithm with Many Targets and Its Use in Weighted Matching Algorithms. In: Meyer auf der Heide, F. (ed.) ESA 2001. LNCS, vol. 2161, pp. 242–253. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  7. 7.
    Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated Testing Based on Java Predicates. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA 2002). IEEE, Rome (2002)Google Scholar
  8. 8.
    Marinov, D., Khurshid, S.: TestEra: A Novel Framework for Automated Testing of Java Programs. Presented at Proceedings of ASE-2001: The 16th IEEE Conference on Automated Software Engineering, Coronado, CA, USA (2001)Google Scholar
  9. 9.
    Dick, J., Faivre, A.: Automating the Generation and Sequencing of Test Cases from Model-Based Specfications. In: Larsen, P.G., Woodcock, J.C.P. (eds.) FME 1993. LNCS, vol. 670, pp. 268–284. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  10. 10.
    Friedman, G., Hartman, A., Nagin, K., Shiran, T.: Projected State Machine Coverage for Software Testing. In: Frankl, P.G. (ed.) Proceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis (ISSTA-02). SOFTWARE ENGINEERING NOTES, vol. 27, 4, pp. 134–143. ACM Press, New York (2002)Google Scholar
  11. 11.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  12. 12.
    Gargantini, A., Riccobene, E., Rinzivillo, S.: Using Spin to Generate tests from ASM Specifications. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 263–277. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  13. 13.
    Sidhu, D.P., Leung, T.-K.: Formal Methods for Protocol Testing: A Detailed Study. IEEE Transactions on Software Engineering 15, 413–426 (1989)CrossRefGoogle Scholar
  14. 14.
    Petrenko, A.: Fault Model-Driven Test Derivation from Finite State Models: Annotated Bibliography. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 196–205. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  15. 15.
    Bourhr, C., Dssouli, R., Aboulhamid, E. M.: Automatic test generation for EFSM-based systems, Publication departementale 1043, Departement IRO, Universite de Montreal (August 1996)Google Scholar
  16. 16.
    Cheng, K.-T., Krishnakumar, A.S.: Automatic generation of functional vectors using the extended finite state machine model. ACM Transactions on Design Automation of Electronic Systems 1, 57–79 (1996)CrossRefGoogle Scholar
  17. 17.
    Petrenko, A., Yevtushenko, N., Bochmann, G.v.: Testing deterministic implementations from nondeterministic FSM specifications. Presented at Proc. IFIP TC6 9th International Workshop on Testing of Communicating Systems, Darmstadt, Germany (1996)Google Scholar
  18. 18.
    Tretmans, J., Belinfante, A.: Automatic testing with formal methods. Presented at EuroSTAR 1999: 7th European Int. Conference on Software Testing, Analysis & Review, Barcelona, Spain (1999)Google Scholar
  19. 19.
    Brinksma, E., Tretmans, J.: Testing Transition Systems: An Annotated Bibliography. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 187–195. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  20. 20.
    Fernandez, J.C., Jard, C., Jéron, T., Viho, C.: An experiment in automatic generation of test suites for protocols with verification technology. Science of Computer Programming - Special Issue on COST247, Verification and Validation Methods for Formal Descriptions 29, 123–146 (1997)Google Scholar
  21. 21.
    Petrenko, A., Yevtushenko, N., Huo, J.L.: Testing Transition Systems with Input and Output Testers. Presented at Proc. IFIP TC6 9th International Workshop on Testing of Communicating Systems, Sophia Antipolis, France (2003)Google Scholar
  22. 22.
    Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accomodates both runtime assertion checking and formal verification, Technical Report TR #03-04 Department of Computer Science, Iowa State University (March 2003)Google Scholar
  23. 23.
    Meyer, B.: Eiffel: The Language. Prentice Hall, New York (1992)zbMATHGoogle Scholar
  24. 24.
    M. M. Systems. JMSAssert (2002)Google Scholar
  25. 25.
    Kramer, R.: iContract – the Java Designs by Contract tool. In: Proc. Technology of Object- Oriented Languages and Systems, presented at Proc. Technology of Object-Oriented Languages and Systems, TOOLS 26, Santa Barbara, CA (1998)Google Scholar
  26. 26.
    Duncan, A., Hoelzle, U.: Adding Contracts to Java with Handshake, University of California, Santa Barbara. Computer Science, Technical Report TRCS98-32, December 9 (1998)Google Scholar
  27. 27.
    Bartetzko, D., Fischer, C., Moller, M., Wehrheim, H.: Jass - Java with assertions. In: Workshop on Runtime Verification held in conjunction with the 13th onference on Computer Aided Verification, CAV 2001 (2001)Google Scholar
  28. 28.
    Corporation, P.: Using design by contract to automate Java software and component testing (February 2003)Google Scholar
  29. 29.
    Edwards, S.H.: A framework for practical, automated black-box testing of component based software. Software Testing, Verification and Reliability 11 (2001)Google Scholar
  30. 30.
    Vries, R.G.d., Tretmans, J.: On-the-fly conformance testing using Spin. Software Tools for Technology Transfer 2, 382–393 (2000)zbMATHCrossRefGoogle Scholar
  31. 31.
    Tan, Q.M., Petrenko, A.: Test Generation for Specifications Modeled by Input/Output Automata. In: Proc. IFIP 11th Int. Conf. on Testing of Communicating Systems, IWTCS 1998, Russia (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Mike Barnett
    • 1
  • Wolfgang Grieskamp
    • 1
  • Lev Nachmanson
    • 1
  • Wolfram Schulte
    • 1
  • Nikolai Tillmann
    • 1
  • Margus Veanes
    • 1
  1. 1.Foundations of Software EngineeringMicrosoft ResearchRedmondUSA

Personalised recommendations