Optimal strategies for testing nondeterministic systems

ABSTRACT

This paper deals with testing of nondeterministic software systems. We assume that a model of the nondeterministic system is given by a directed graph with two kind of vertices: states and choice points. Choice points represent the nondeterministic behaviour of the implementation under test (IUT). Edges represent transitions. They have costs and probabilities. Test case generation in this setting amounts to generation of a game strategy. The two players are the testing tool (TT) and the IUT. The game explores the graph. The TT leads the IUT by selecting an edge at the state vertices. At the choice points the control goes to the IUT. A game strategy decides which edge should be taken by the TT in each state. This paper presents three novel algorithms 1) to determine an optimal strategy for the bounded reachability game, where optimality means maximizing the probability to reach any of the given final states from a given start state while at the same time minimizing the costs of traversal; 2) to determine a winning strategy for the bounded reachability game, which guarantees that given final vertices are reached, regardless how the IUT reacts; 3) to determine a fast converging edge covering strategy, which guarantees that the probability to cover all edges quickly converges to 1 if TT follows the strategy.

REFERENCES

• 1: Rajeev Alur , Costas Courcoubetis , Mihalis Yannakakis, Distinguishing tests for nondeterministic and probabilistic machines, Proceedings of the twenty-seventh annual ACM symposium on Theory of computing, p.363-372, May 29-June 01, 1995, Las Vegas, Nevada, United States [doi>10.1145/225058.225161]
• 2: C. Artho, D. Drusinsky, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, G. Rosu, and W. Visser. Experiments with test case generation and runtime analysis. In Börger, Gargantini, and Riccobene, editors, Abstract State Machines 2003, volume 2589 of LNCS, pages 87--107. Springer, 2003.
• 3: AsmL. URL: http://research.microsoft.com/fse/AsmL/.
• 4: 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.
• 5: Mike Barnett , Wolfram Schulte, Runtime verification of .NET contracts, Journal of Systems and Software, v.65 n.3, p.199-208, 15 March 2003 [doi>10.1016/S0164-1212(02)00041-9]
• 6: Boris Beizer, Software testing techniques (2nd ed.), Van Nostrand Reinhold Co., New York, NY, 1990
• 7: D. Box. Code name Indigo: A guide to developing and running connected systems with Indigo. MSDN magazine, 2003. URL: http://msdn.microsoft.com/msdnmag/.
• 8: 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
• 9: Anne Condon, The complexity of stochastic games, Information and Computation, v.96 n.2, p.203-224, Feb. 1992 [doi>10.1016/0890-5401(92)90048-K]
• 10: Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990
• 11: Jean-Claude Fernandez , Claude Jard , Thierry Jéron , César Viho, An experiment in automatic generation of test suites for protocols with verification technology, Science of Computer Programming, v.29 n.1-2, p.123-146, July 1997 [doi>10.1016/S0167-6423(96)00032-9]
• 12: Jerzy Filar , Koos Vrieze, Competitive Markov decision processes, Springer-Verlag New York, Inc., New York, NY, 1996
• 13: A. Gibbons. Algorithmic Graph Theory. Cambridge University Press, 1985.
• 14: Raymond Greenlaw , H. James Hoover , Walter L. Ruzzo, Limits to parallel computation: P-completeness theory, Oxford University Press, Inc., New York, NY, 1995
• 15: Wolfgang Grieskamp , Yuri Gurevich , Wolfram Schulte , Margus Veanes, Generating finite state machines from abstract state machines, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 16: Susumu Fujiwara , Gregor von Bochmann, Testing Non-Deterministic State Machines with Fault Coverage, Proceedings of the IFIP TC6/WG6.1 Fourth International Workshop on Protocol Test Systems IV, p.267-280, October 15-17, 1991
• 17: Yuri Gurevich, Evolving algebras 1993: Lipari guide, Specification and validation methods, Oxford University Press, Inc., New York, NY, 1995
• 18: 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.
• 19: N. Immerman. Number of quantifiers is better than number of tape cells. Journal of Computer and System Sciences, 22(3):384--406, 1981.
• 20: N. D. Jones and W. T. Laaser. Complete problems for deterministic polynomial time. Theoretical Computer Science, 3(1):105--117, 1976.
• 21: V. V. Kuliamin, A. K. Petrenko, A. S. Kossatchev, and I. B. Bourdonov. UniTesK: Model based testing in industrial practice. In 1st European Conference on Model Driven Software Engineering, pages 55--63, Nuremberg, Germany, December 2003.
• 22: D. Lee and M. Yannakakis. Principles and methods of testing finite state machines -- a survey. In Proceedings of the IEEE, volume 84, pages 1090--1123, Berlin, Aug 1996.
• 23: Kurt Mehlhorn , Guido Schäfer, A Heuristic for Dijkstra's Algorithm with Many Targets and Its Use in Weighted Matching Algorithms, Proceedings of the 9th Annual European Symposium on Algorithms, p.242-253, August 28-31, 2001
• 24: Martin L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, John Wiley & Sons, Inc., New York, NY, 1994
• 25: H. Robinson. Model-based testing home page. URL: http://www.geocities.com/model_based_testing/.
• 26: Deepinder P. Sidhu , Ting-kau Leung, Formal Methods for Protocol Testing: A Detailed Study, IEEE Transactions on Software Engineering, v.15 n.4, p.413-426, April 1989 [doi>10.1109/32.16602]
• 27: 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.
• 28: 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.
• 29: Wang Yi , Kim Guldstrand Larsen, Testing Probabilistic and Nondeterministic Processes, Proceedings of the IFIP TC6/WG6.1 Twelth International Symposium on Protocol Specification, Testing and Verification XII, p.47-61, June 22-25, 1992
• 30: Fan Zhang , To-yat Cheung, Optimal Transfer Trees and Distinguishing Trees for Testing Observable Nondeterministic Finite-State Machines, IEEE Transactions on Software Engineering, v.29 n.1, p.1-14, January 2003 [doi>10.1109/TSE.2003.1166585]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Statistical methods
      D.2.5 Testing and Debugging
          Subjects: Testing tools (e.g., data generators, coverage testing)

General Terms:
Algorithms, Reliability

Keywords:
abstract state machines, optimal game strategies, probabilistic nondeterministic finite state machines