Generating optimal distinguishing sequences with a model checker

ABSTRACT

This paper presents an approach for the automatic generation of shortest Distinguishing Sequences (DS) with the Uppaal model checker. The presented method is applicable to a large number of extended finite state machines and it will find an optimal result, if a DS sequence exists for the considered automaton. Our approach is situated in an integrated testing environment that is used to generate checking sequences. The generation method is based on a DS model, which is derived from the same test model that is used for generating test cover sets. The problem of generating DS is reduced to the definition of a DS model and for this reason the complexity of our approach depends mainly on the used model checking algorithm. This means, that the presented method is automatically improved, when the model checking algorithm is improved. This includes the generation of optimal DS depending on the ability of the model checker to produce optimal results.

REFERENCES

• 1: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
• 2: Johan Bengtsson , Kim Larsen , Fredrik Larsson , Paul Pettersson , Wang Yi, UPPAAL—a tool suite for automatic verification of real-time systems, Proceedings of the DIMACS/SYCON workshop on Hybrid systems III : verification and control: verification and control, p.232-243, July 1996, New Brunswick, NeW Jersey, United States
• 3: Gregor V. Bochmann , Alexandre Petrenko, Protocol testing: review of methods and relevance for software testing, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.109-124, August 17-19, 1994, Seattle, Washington, United States [doi>10.1145/186258.187153]
• 4: M. Clarke, O. Grumberg, D. A. Peled. Model Checking. MIT Press. Boston, 2000.
• 5: D. Lee , M. Yannakakis, Testing Finite-State Machines: State Identification and Verification, IEEE Transactions on Computers, v.43 n.3, p.306-320, March 1994 [doi>10.1109/12.272431]
• 6: E. F. Moore. Gedanken-Experiments on Sequential Machines. Automata Studies (Annals of Mathematics Studies), (34), 1956.
• 7: A. D. Friedman, P. R. Menon, Fault Detection in Digital Circuits, Prentice Hall, Englewood Cliffs, NJ, 1971
• 8: 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]
• 9: Dechang Sun , Bapiraju Vinnakota , Wanli Jiang, Fast state verification, Proceedings of the 35th annual conference on Design automation, p.619-624, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277205]
• 10: Michaela Huhn Tilo Mücke. Generation of Optimized Testsuites for UML Statecharts with Time. In Robert M. Hierons Roland Groz, editor, Testing of Communicating Systems, Berlin, March 2004. Springer.
• 11: Hasan Ural, Formal methods for test sequence generation, Computer Communications, v.15 n.5, p.311-325, June 1992 [doi>10.1016/0140-3664(92)90092-S]
• 12: F. C. Hennie, Fault-Detecting Experiments for Sequential Circuits, Proc. 5th Annual Symposium on Switching Circuit Theory and Logical Design, NJ, 1964
• 13: Krishan Sabnani , Anton Dahbura, A protocol test generation procedure, Computer Networks and ISDN Systems, v.15 n.4, p.285-297, Sept. 1988 [doi>10.1016/0169-7552(88)90064-5]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
      D.2.5 Testing and Debugging

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems

General Terms:
Algorithms, Verification

Keywords:
distinguishing sequence, extended finite state machines, model checking, state identification, test generation, verification