Online testing with model programs

ABSTRACT

Online testing is a technique in which test derivation from a model program and test execution are combined into a single algorithm. We describe a practical online testing algorithm that is implemented in the model-based testing tool developed at Microsoft Research called Spec Explorer. Spec Explorer is being used daily by several Microsoft product groups. Model programs in Spec Explorer are written in the high level specification languages AsmL or Spec\#. We view model programs as implicit definitions of interface automata. The conformance relation between a model and an implementation under test is formalized in terms of refinement between interface automata. Testing then amounts to a game between the test tool and the implementation under test.

REFERENCES

• 1: Spec Explorer. URL:http://research.microsoft.com/specexplorer, released January 2005.
• 2: Rajeev Alur , Thomas A. Henzinger , Orna Kupferman , Moshe Y. Vardi, Alternating Refinement Relations, Proceedings of the 9th International Conference on Concurrency Theory, p.163-178, September 08-11, 1998
• 3: M. Barnett, W. Grieskamp, L. Nachmanson, W. Schulte, N. Tillmann, and M. Veanes. Towards a tool environment for model-based testing with AsmL. In Petrenko and Ulrich, editors, Formal Approaches to Software Testing, FATES 2003, volume 2931 of LNCS, pages 264--280. Springer, 2003.
• 4: M. Barnett, R. Leino, and W. Schulte. The Spec# programming system: An overview. In M. Huisman, editor, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices: International Workshop, CASSIS 2004, volume 3362 of LNCS, pages 49--69. Springer, 2005.
• 5: A. Blass, Y. Gurevich, L. Nachmanson, and M. Veanes. Play to test. Technical Report MSR-TR-2005-04, Microsoft Research, January 2005.
• 6: Ed Brinksma , Jan Tretmans, Testing transition systems: an annotated bibliography, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
• 7: C. Campbell, W. Grieskamp, L. Nachmanson, W. Schulte, N. Tillmann, and M. Veanes. Model-based testing of object-oriented reactive systems with Spec Explorer. Tech. Rep. MSR-TR-2005-59, Microsoft Research, 2005.
• 8: C. Campbell and M. Veanes. State exploration with multiple state groupings. In D. Beauquier, E. Börger, and A. Slissenko, editors, 12th International Workshop on Abstract State Machines, ASM'05, March 8--11, 2005, Laboratory of Algorithms, Complexity and Logic, Créteil, France, pages 119--130, 2005.
• 9: C. Campbell, M. Veanes, J. Huo, and A. Petrenko. Multiplexing of partially ordered events. In F. Khendek and R. Dssouli, editors, 17th IFIP International Conference on Testing of Communicating Systems, TestCom 2005, volume 3502 of LNCS, pages 97--110. Springer, 2005.
• 10: L. de Alfaro. Game models for open systems. In N. Dershowitz, editor, Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, volume 2772 of LNCS, pages 269--289. Springer, 2004.
• 11: Luca de Alfaro , Thomas A. Henzinger, Interface automata, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 12: L. Franzen, J. Tretmans, and T. Willemse. Test generation based on symbolic specifications. In J. Grabowski and B. Nielsen, editors, Proceedings of the Workshop on Formal Approaches to Software Testing (FATES 2004), pages 3--17, Linz, Austria, September 2004. To appear in LNCS.
• 13: Wolfgang Grieskamp , Yuri Gurevich , Wolfram Schulte , Margus Veanes, Generating finite state machines from abstract state machines, ACM SIGSOFT Software Engineering Notes, v.27 n.4, July 2002
• 14: W. Grieskamp, N. Tillmann, and M. Veanes. Instrumenting scenarios in a model-driven development environment. Information and Software Technology, 2004. In press, available online.
• 15: Yuri Gurevich, Evolving algebras 1993: Lipari guide, Specification and validation methods, Oxford University Press, Inc., New York, NY, 1995
• 16: Y. Gurevich, B. Rossman, and W. Schulte. Semantic essence of AsmL. Theoretical Computer Science, 2005. Preliminary version available as Microsoft Research Technical Report MSR-TR-2004-27.
• 17: A. Hartman and K. Nagin. Model driven testing - AGEDIS architecture interfaces and tools. In 1st European Conference on Model Driven Software Engineering, pages 1--11, Nuremberg, Germany, December 2003.
• 18: Lev Nachmanson , Margus Veanes , Wolfram Schulte , Nikolai Tillmann , Wolfgang Grieskamp, Optimal strategies for testing nondeterministic systems, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 19: S. Tasiran and S. Qadeer. Runtime refinement checking of concurrent data structures. Electronic Notes in Theoretical Computer Science, 113:163--179, January 2005. Proceedings of the Fourth Workshop on Runtime Verification (RV 2004).
• 20: J. Tretmans and A. Belinfante. Automatic testing with formal methods. In EuroSTAR'99: 7th European Int. Conference on Software Testing, Analysis & Review, Barcelona, Spain, November 8--12, 1999.
• 21: J. Tretmans and E. Brinksma. TorX: Automated model based testing. In 1st European Conference on Model Driven Software Engineering, pages 31--43, Nuremberg, Germany, December 2003.
• 22: M. van der Bij, A. Rensink, and J. Tretmans. Compositional testing with ioco. In A. Petrenko and A. Ulrich, editors, Formal Approaches to Software Testing: Third International Workshop, FATES 2003, volume 2931 of LNCS, pages 86--100. Springer, 2004.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Testing tools (e.g., data generators, coverage testing)

General Terms:
Reliability, Verification

Keywords:
conformance testing, interface automata, runtime verification