This Article 
 Bibliographic References 
 Add to: 
Confirming Configurations in EFSM Testing
January 2004 (vol. 30 no. 1)
pp. 29-42

Abstract—In this paper, we investigate the problem of configuration verification for the extended FSM (EFSM) model. This is an extension of the FSM state identification problem. Specifically, given a configuration (“state vector”) 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 of a particular EFSM transition. We demonstrate that this 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. We introduce notions of EFSM projections and products and, based on these notions, we develop a theoretical framework for determining configuration-confirming sequences. The proposed approach is illustrated on a realistic example.

[1] A. Ek, J. Grabowski, D. Hogrefe, R. Jerome, B. Koch, and M. Schmitt, Towards the Industrial Use of Validation Techniques and Automatic Test Generation Methods for SDL Specifications Proc. Eighth SDL Forum, pp. 245-259, 1997.
[2] A. Kerbrat, T. Jéron, and R. Groz, Automated Test Generation from SDL Specifications Proc. Ninth SDL Forum, pp. 135-151, 1999.
[3] A. Petrenko, G.v. Bochmann, and M. Yao, On Fault Coverage of Tests for Finite State Specifications Computer Networks and ISDN Systems, vol. 29, pp. 81-106, Dec. 1996.
[4] D. Lee and M. Yannakakis, Principles and Methods of Testing Finite State Machines, a Survey Proc. IEEE, vol. 84, no. 8, pp. 1090-1123, Aug. 1996.
[5] E.P. Hsieh, Checking Experiments for Sequential Machines IEEE Trans. Computers, vol. 20, no. 10, pp. 1152-1166, 1971.
[6] D. Lee and M. Yannakakis, Testing Finite-State Machines: State Identification and Verification IEEE Trans. Computers, vol. 43, no. 3, pp. 306-320, Mar. 1994.
[7] A. Gill, Introduction to the Theory of Finite-State Machines, p. 207. McGraw-Hill, 1962.
[8] A. Petrenko and N. Yevtushenko, Test Suite Generation for a Given Type of Implementation Errors Proc. IFIP XII Int'l Conf. Protocol Specification, Testing, and Verification, pp. 229-243, 1992.
[9] W.R. Mark, L. McMillan, and G. Bishop, "Post-Rendering 3D Warping," M. Cohen and D. Zeltzer, eds., Proc. 1997 Symp. Interactive 3D Graphics, ACM Press, New York, 1997, pp. 7-16.
[10] H. Ural and A. Williams, Test Generation by Exposing Control and Data Dependencies within System Specifications in SDL Proc. Sixth IFIP Conf. Formal Description Techniques, pp. 339-354, 1993.
[11] H. Ural, Test Sequence Selection Based on Static Data Flow Analysis Computer Comm., vol. 10, no. 5, pp. 234-242, 1987.
[12] R.E. Miller and S. Paul, Generating Conformance Test Sequences for Combined Control and Data Flow of Communication Protocols Proc. IFIP XII Int'l Conf. Protocol Specification, Testing and Verification, pp. 13-27, 1992.
[13] K.-T. Cheng and A.S. Krishnakumar, Automatic Functional Test Generation Using the Extended Finite State Machine Model Proc. 30th Design Automation Conf., pp. 86-91, 1993.
[14] W. Chun and P.D. Amer, Test Case Generation for Protocols Specified in Estelle Proc. IFIP Conf. Formal Description Techniques, vol. III, pp. 191-206, 1991.
[15] P. Qixiang, C. Shiduan, and J. Yuchui, Protocol Conformance Test Suite Generation Proc. ICCT'96, Int'l Conf. Comm. Technology, vol. 1, pp. 218-222, 1996.
[16] R.E. Miller and Y. Xue, Bridging the Gap between Formal Specification and Analysis of Communication Protocols Proc. IEEE 15th Ann. Int'l Phoenix Conf. Computers and Comm., pp. 225-231, 1996.
[17] C.-M. Huang and M.-S. Chiang, Protocol Test Sequence Generation for EFSM-Specified Protocols Proc. 1994 Int'l Computer Symp., vol. 2, pp. 842-847, 1994.
[18] L.-S. Koh and M.T. Liu, Test Path Selection Based on Effective Domains Proc. Int'l Conf. Network Protocols, pp. 64-71, 1994.
[19] C.-J. Wang, L.-S. Koh, and M.T. Liu, Protocol Validation Tools as Test Case Generators Proc. Seventh Int'l Workshop Protocol Test Systems, pp. 155-170, 1994.
[20] S.T. Chanson and J. Zhu, Automatic Protocol Test Suite Derivation Proc. Conf. Computer Comm., vol. 2, pp. 792-799, 1994.
[21] S.T. Chanson and J. Zhu, A Unified Approach to Protocol Test Sequence Generation Proc. INFOCOM'93 Conf., vol. 1, pp. 106-114, 1993.
[22] X. Li, T. Higashino, M. Higuchi, and K. Taniguchi, Automatic Generation of Extended UIO Sequences for Communication Protocols in an EFSM Model Proc. Seventh Int'l Workshop Protocol Test Systems, pp. 225-240, 1994.
[23] T. Ramalingom, A. Das, and K. Thulasiraman, Context Independent Unique Sequences Generation for Protocol Testing Proc. Int'l Conf. Computer Comm. 15th Ann. Joint Conf. IEEE Computer Soc., vol. 3, pp. 1141-1148, 1996.
[24] W. Chun and P.D. Amer, Improvements on UIO Sequence Generation and Partial UIO Sequences Proc. IFIP XII Int'l Conf. Protocol Specification, Testing, and Verification, pp. 245-260, 1992.
[25] P. Camurati, M. Gilli, P. Prinetto, and M.S. Reorda, Model Checking and Graph Theory in Sequential ATPG Proc. Workshop in Computer-Aided Verification Conf. (CAV '90), DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 3, pp. 505-517, 1991.
[26] 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, vol. 12, pp. 267-289, 1998.
[27] A. Petrenko, N. Yevtushenko, and G.v. Bochmann, Testing Deterministic Implementations from their Nondeterministic Specifications Proc. IFIP Ninth Int'l Workshop Testing Comm. Systems, pp. 125-140, 1996.
[28] R. Alur, C. Courcoubetis, and M. Yannakakis, Distinguishing Tests for Nondeterministic and Probabilistic Machines Proc. 27th ACM Symp. Theory of Computing, pp. 363-372, 1995.
[29] H. Cho, G. Hachtel, S.-W. Jeong, B. Plessier, E. Schwarz, and F. Somenzi, Results on the Interface Between Formal Verification and ATPG Proc. Workshop in Computer-Aided Verification Conf. (CAV '90), DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 3, pp. 615-627, 1991.
[30] M. Clatin, R. Groz, M. Phalippou, and R. Thummel, Two Approaches Linking a Test Generation Tool with Verification Techniques Proc. IFIP Eighth Int'l Workshop Protocol Test Systems, 1995.
[31] S. Huang, D. Lee, and M. Staskauskas, Validation-Based Test Sequence Generation for Networks of Extended Finite State Machines Proc. IFIP Conf. Formal Description Techniques, vol. IX, pp. 403-418, 1996.
[32] J.-C. Fernandez, C. Jard, T. Jéron, and C. Viho, An Experiment in Automatic Generation of Test Suites for Protocols with Verification Technology Science of Computer Programming, vol. 29, pp. 123-146, 1996.
[33] A. Petrenko, S. Boroday, and R. Groz, Confirming Configurations in EFSM Proc. IFIP Joint Int'l Conf. Formal Description Techniques (FORTE XII) for Distributed Systems and Comm. Protocols, and Protocol Specification, Testing, and Verification (PSTV XIX), pp. 5-24, 1999.
[34] P. Stocks and D. Carrington, A Framework for Specification-Based Testing IEEE Trans. Software Eng., vol. 22, no. 11, pp. 777-793, 1996.
[35] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, May 1997.
[36] G. Luo, G.V. Bochman, and A. Petrenko, “Test Selection Based on Communicating Nodetermistic Finite State Machines Using a Generalized wp-Method,” IEEE Trans. Software Eng., vol. 20, no. 2, pp. 149-162, Feb. 1994.
[37] G.v. Bochmann and A. Petrenko, Protocol Testing: Review of Methods and Relevance for Software Testing Proc. ACM Int'l Symp. Software Testing and Analysis, pp. 109-124, 1994.
[38] N. Yevtushenko and A. Petrenko, A Method of Constructing a Test Experiment for an Arbitrary Deterministic Automaton Automatic Control and Computer Science, vol. 24, no. 5, pp. 65-68, 1990.
[39] M.P. Vasilevsky, Failure Diagnosis of Automata Cybernetics, no. 4, pp. 653-665, 1973.
[40] T.S. Chow, Test Software Design Modeled by Finite State Machines IEEE Trans. Software Eng., vol. 4, no. 3, pp. 178-187, 1978.
[41] S. Fujiwara, V.G. Bochmann, F. Khendek, M. Amalou, and A. Ghedamsi, “Test Selection Based on Finite State Machine Model,” IEEE Trans. Software Eng., vol. 17, no. 6, pp. 591-603, June 1991.
[42] D.P. Sidhu and T.K. Leung, Formal Methods for Protocol Testing: A Detailed Study IEEE Trans. Software Eng., vol. 15, no. 4, pp. 413-426, Apr. 1991.
[43] S. Warshall, A Theorem on Boolean Matrices J. ACM, vol. 9, pp. 11-12, 1962.
[44] J.F. Poage and E.J. McCluskey, Derivation of Optimum Test Sequences for Sequential Machines Proc. Fifth Ann. Symp. Switching Theory and Logical Design, pp. 121-132, 1964.
[45] ITU-T, Recommendation Z.100-Specification and Description Language (SDL), Geneva, 1994.
[46] ISO/IEC, Information Processing Systems, Estelle A Formal Description Technique based on Extended State Transition Model, ISO 9074, 1997.
[47] D. Harel and A. Naamad, The STATEMATE Semantics of Statecharts ACM Trans. Software Eng. and Methodology, vol. 5, no. 4, pp. 293-333, 1996.
[48] OMG, Unified Modelling Language, version 1.4. OMG Standard, Nov. 2002.
[49] A.S. Krishnakumar, Reachability and Recurrence in Extended Finite State Machines: Modular Vector Addition Systems Proc. Fifth Int'l Conf. Computer Aided Verification, pp. 110-122, 1993.
[50] E.M. Clarke, Jr., O. Grumberg, and D. Peled, Model Checking, p. 314. The MIT Press, 1999.
[51] Object Geode SDL Simulator Reference Manual, Telelogic AB, 2000.
[52] S. Boroday, R. Groz, A. Petrenko, and Y.-M. Quemener, Techniques for Abstracting SDL Specifications Proc. Third SAM (SDL And MSC) Workshop, pp. 141-157, 2002.
[53] V. Rusu, L. Du Bousquet, and T. Jéron, An Approach to Symbolic Test Generation Proc. Second Int'l Conf. Integrating Formal Methods (IFM'00), pp. 338-357, 2000.
[54] R. Alur, T.A. Henzinger, and P.-H. Ho, “Automatic Symbolic Verification of Embedded Systems,” IEEE Trans. Software Eng., vol. 22, no. 3, Mar. 1996.
[55] V. Okun, P.E. Black, and Y. Yesha, Testing with Model Checker: Insuring Fault Visibility Proc. Int'l Conf. System Science, Applied Mathematics and Computer Science, and Power Eng. Systems, pp. 1351-1356, 2002.
[56] S. Boroday, A. Petrenko, R. Groz, and Y.-M. Quemener, Test Generation for CEFSM Combining Specification and Fault Coverage Proc. IFIP XIV Int'l Conf. Testing of Comm. Systems (TestCom 2002), pp. 355-372, 2002.
[57] R. Groz and N. Risser, Eight Years of Experience in Test Generation from FDTs Using TVEDA Proc. Int'l Conf. Formal Description Techniques for Distributed Systems and Comm. Protocols, and Protocol Specification, Testing, and Verification, pp. 465-480, 1997.
[58] L. Doldi, Validation of Communications Systems with SDL: The Art of SDL Simulation and Reachability Analysis, p. 310. John Wiley and Sons, 2003.

Index Terms:
Formal methods, test design, model checking, extended finite state machine, functional testing, conformance testing, test derivation, state identification, model-based testing.
Alexandre Petrenko, Sergiy Boroday, Roland Groz, "Confirming Configurations in EFSM Testing," IEEE Transactions on Software Engineering, vol. 30, no. 1, pp. 29-42, Jan. 2004, doi:10.1109/TSE.2004.1265734
Usage of this product signifies your acceptance of the Terms of Use.