Abstract
In this paper we investigate the problem of configuration distinguishability for the EFSM model, specifically, given a configuration and an arbitrary set of configurations, determine an input sequence such that the EFSM in the given configuration produces an output sequence different from that of the configurations in the given set or at least in a maximal proper subset. Such a sequence can be used in a test case to confirm the destination configuration. We demonstrate that the distinguishability problem could be reduced to the EFSM traversal problem, so that the existing methods and tools developed in the context of model checking become applicable. The theoretical framework for determining configuration-confirming sequences based on projections and products of EFSMs is presented. Our approach can be implemented in a number of heuristic test derivation strategies.
Chapter PDF
Similar content being viewed by others
References
A. Ek, J. Grabowski, D. Hogrefe, R. Jerome, B. Koch, M. Schmitt, Towards the industrial use of validation techniques and automatic test generation methods for SDL specifications, Proceedings of SDL’97: Time for Testing - SDL, MSC and Trends, Elsevier, 1997.
A. Kerbrat, T. Jéron, R. Groz, Automated test generation from SDL specifications, Proceedings of SDL’99, Elsevier, 1999.
A. Petrenko, G. v. Bochmann, and M. Yao, On fault coverage of tests for finite state specifications, Computer Networks and ISDN Systems, 29, December 1996, pp. 81–106.
D. Lee, M. Yannakakis, Principles and methods of testing finite state machines, a survey, Proceedings of the IEEE, vol. 84, 8, 1996, pp. 1090–1123.
E. P. Hsieh, Checking experiments for sequential machines, IEEE Transactions on Computers, Vol. C-20, 10, 1971, pp. 1152–1166.
D. Lee, M. Yannakakis, Testing finite-state machines: state identification and verification, IEEE Transactions on Computers, Vol. 43, 3, 1994, pp. 306–320.
A. Gill, Introduction to the theory of finite-state machines, Mc Graw-Hill, New York, 1962.
A. Petrenko, N. Yevtushenko, Test suite generation for a given type of implementation errors, Proceedings of the IFIP XII International Conference on Protocol Specification, Testing and Verification, 1992, pp. 229–243.
C.-J. Wang and M. T. Liu, Generating test cases for EFSM with given fault model, Proceedings of the IEEE 1NFOCOM’93, 1993, pp. 774–781.
l0. H. Ural, A. Williams, Test generation by exposing control and data dependencies within system specifications in SDL, Proceedings of the IFIP Conference on Formal Description Techniques, 1993.
H. Ural, Test sequence selection based on static data flow analysis, Computer Communications, Vol. 10, No. 5, 1987.
R. E. Miller, and S. Paul, Generating conformance test sequences for combined control and data flow of communication protocols, Proceedings of IFIP XII International Conference on Protocol Specification, Testing and Verification, 1992, pp. 13–27.
K.-T. Cheng, A. S. Krishnakumar, Automatic functional test generation using the extended finite state machine model, Proceedings of the 30th Design Automation Conference, 1993, pp. 86–91.
W. Chun, P. D. Amer, Test case generation for protocols specified in Estelle, Proceedings of the IFIP Conference on Formal Description Techniques, III, 1991, pp. 191–206.
P. Qixiang, C. Shiduan, J. Yuchui, Protocol conformance test suite generation, Proceedings of ICCT’96, International Conference on Communication Technology, Vol. 1, 1996, pp. 218–222.
R. E. Miller, Y. Xue, Bridging the gap between formal specification and analysis of communication protocols,Proceedings of the 1996 IEEE Fifteenth Annual International Phoenix Conference on Computers and Communications, pp. 225–231.
C.-M. Huang, M.-S. Chiang, Protocol test sequence generation for EFSM-specified protocols, Proceedings of the International Computer Symposium Conference, vol. 2, 1994, pp. 842–847.
L.-S. Koh, M. T. Liu, Test path selection based on effective domains, Proceedings of ICNP, International Conference on Network Protocols, 1994, pp. 64–71.
C.-J. Wang, L.-S. Koh, M. T. Liu, Protocol validation tools as test case generators, Proceedings of the 7th International Workshop on Protocol Test Systems, 1994, pp. 155–170.
S. T. Chanson, J. Zhu, Automatic protocol test suite derivation, Proceedings of INFOCOM’94, Conference on Computer Communications, vol. 2, 1994, pp. 792–799.
S. T. Chanson, J. Zhu, A unified approach to protocol test sequence generation, Proceedings of INFOCOM’93, vol. 1, 1993, pp. 106–114.
X. Li, T. Higashino, M. Higuchi, K. Taniguchi, Automatic generation of extended UIO sequences for communication protocols in an EFSM model, Proceedings of the 7th International Workshop on Protocol Test Systems, 1994, pp. 225–240.
T. Ramalingom, A. Das, K. Thulasiraman, A unified test case generation method for the EFSM model using context independent unique sequences, Proceedings of the IFIP 8’ International Workshop on Protocol Test Systems, 1995.
W. Chun, P. D. Amer, Improvements on UIO sequence generation and partial UIO sequences, Proceedings of the IFIP XII International Conference on Protocol Specification, Testing and Verification, 1992, pp. 245–260.
P. Camurati, M. Gilli, P. Prinetto, and M. S. Reorda, Model checking and graph theory in sequential ATPG, Proceedings of CAV’90, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, 1991, pp. 505–517.
G. Cabodi, P. Camurati, F. Corno, P. Prinetto, and M. S. Reorda, The general product machine: a new model for symbolic FSM traversal, Formal Methods in System Design, 12, 1998, pp. 267–289.
A. Petrenko, N. Yevtushenko, and G. v. Bochmann, Testing deterministic implementations from their nondeterministic specifications, Proceedings of the IFIP 9th International Workshop on Testing Communicating Systems, 1996, pp. 125–140.
R. Alur, C. Courcoubetis, and M. Yannakakis, Distinguishing tests for nondeterministic and probabilistic machines, Proceedings of the 27th ACM Symposium on Theory of Computing, 1995, pp. 363–372.
H. Cho, G. Hachtel, S.-W. Jeong, B. Plessier, E. Schwarz, F. Somenzi, Results on the interface between formal verification and ATPG, Proceedings of CAV’90, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, 1991, pp. 615–627.
M. Clatin, R. Groz, M. Phalippou, R. Thummel, Two approaches linking a test generation tool with verification techniques, Proceedings of the IFIP 8th International Workshop on Protocol Test Systems, 1995.
S. Huang, D. Lee, M. Staskauskas, Validation-based test sequence generation for networks of extended finite state machines, in Proceedings of the IFIP Conference on Formal Description Techniques, IX, 1996, pp. 403–418.
J.-C. Fernandez, C. Jard, T. Jéron, C. Viho, An experiment in automatic generation of test suites for protocols with verification technology, Science of Computer Programming, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Petrenko, A., Boroday, S., Groz, R. (1999). Confirming configurations in EFSM. In: Wu, J., Chanson, S.T., Gao, Q. (eds) Formal Methods for Protocol Engineering and Distributed Systems. PSTV FORTE 1999 1999. IFIP Advances in Information and Communication Technology, vol 28. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35578-8_1
Download citation
DOI: https://doi.org/10.1007/978-0-387-35578-8_1
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5270-0
Online ISBN: 978-0-387-35578-8
eBook Packages: Springer Book Archive