Fast state verification

ABSTRACT

Unique input/output(UIO) sequences are used for state verification and functional test in finite state machines. A UIO sequence for a state s distinguishes it from other states in the FSM. Current algorithms to compute UIO sequences are limited in their applicability to FSMs with binary input symbols such as those found in con trol applications. Execution times of traditional approaches are exponential in the n umber of FSM inputs. We dev elop a new heuristic algorithm to generate UIO sequences for FSMs with binary inputs. Execution time is reduced significantly b y reducing the size of the search space. When a UIO sequence cannot be generated, our algorithm generates a small n umber of functional faults for state verification.

REFERENCES

• 1: D. Lee and M. Yannakakis, "Principles and Methods of Testing Finite State Machines-- A Survey," Proceedings of IEEE, vol. 84, No.8, pp. 1090-1122, August, 1996.
• 2: 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]
• 3: A. V. Aho, A. T. Dahbura, D. Lee and M. U. Uyax, "An Optimization technique for protocol conformance test generation based on UIO sequences and rural Chinese postman tours," IEEE Trans. Communications, vol. 39, No.3, pp. 1604-1615, 1991.
• 4: K.T. Cheng and J. Y. Jou, "Functional Test Generation for Finite State Machines"' International Test Conference, September 1990.
• 5: 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]
• 6: E. Hsieh, "Checking Experiments for Sequential Machines''' IEEE Trans. Computers, vol. C-20, pp.1152- 1166' Oct. 1971.
• 7: Irith Pomeranz , Sudhakar M. Reddy, On achieving a complete fault coverage for sequential machines using the transition fault model, Proceedings of the 28th conference on ACM/IEEE design automation, p.341-346, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127691]
• 8: G. Buonanno , F. Fummi , D. Sciuto , F. Lombardi, FsmTest: functional test generation for sequential circuits, Integration, the VLSI Journal, v.20 n.3, p.303-325, July 1996 [doi>10.1016/0167-9260(96)00006-5]
• 9: B. Vinnakota and J. Andrews, "Fast Fault Translation," IEEE Trans. VLSI Systems, pp.122-133, March 1998.
• 10: R. Lisanke, "Finite-state machine benchmark set," Preliminary benchmark collection, 1987. Available at "htt p://www, cbl. ncsu. edu".
• 11: A. Aho, A.T. Dahbura, D.Lee and M. UmitUyar, "An optimization technique for protocol conformance test generation based on UIO sequences and Rural Chinese Postman Tours," Protocol Specification, Testing and Verification, Vol. VIII, North-HollandTAmsterdam' pp.131-143, 1988.
• 12: Yinan N. Shen , Fabrizio Lombardi , Anton T. Dahbura, Protocol Conformance Testing Using Multiple UIO Sequences, Proceedings of the IFIP WG6.1 Ninth International Symposium on Protocol Specification, Testing and Verification IX, p.131-143, June 06-09, 1989
• 13: D. Schin, Y.-N. Shen and F. Lombardi, "An approach for UIO generation for FSM verification and validation"' Proc. ISCAS, vol. 4, pp.303-306, 1994.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)

Additional Classification:
  B. Hardware
  B.8 Performance and Reliability

  C. Computer Systems Organization

  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

  J. Computer Applications

General Terms:
Algorithms, Design, Experimentation, Measurement, Performance, Theory, Verification

Keywords:
guided search, model checking, verification