Abstract
This paper presents a theory of test coverage and generation from specifications written in EFSMs. We investigate a family of coverage criteria based on the information of control flow and data flow and characterize them in the branching time temporal logic CTL. We discuss the complexity of minimal cost test generation and describe a method for automatic test generation which employs the capability of model checkers to construct counterexamples. Our approach extends the range of applications of model checking from formal verification of finite state systems to test generation from finite state systems.
This research was supported in part by NSF CCR-9988409, NSF CCR-0086147, NSF CISE-9703220, AROD AAD19-01-1-0473, and DARPA ITOMO BIES F33615-00-C-1707.
Partially supported by the Advanced Information Technology Research Center (AITrc) at Korea Advanced Institute of Science and Technology (KAIST).
Chapter PDF
Similar content being viewed by others
References
P. Ammann, P. Black, and W. Majurski, “Using Model Checking to Generate Tests from Specifications,” in Proceedings of 2nd IEEE International Conference on Formal Engineering Methods, pp. 46–54, 1998.
F. Belina and D. Hogrefe, “The CCITT-Specification and Description Language SDL,” Computer Networks and ISDN Systems, Vol. 16, pp. 311–341, 1989.
G.v. Bochmann and A. Petrenko, “Protocol Testing: Review of Methods and Relevance for Software Testing,” in Proceedings of the 1994 International Symposium on Software Testing and Analysis, pp 109–124, 1994.
S. Budkowski and P. Dembinski, “An Introduction to Estelle: a Specification Language for Distributed Systems,” Computer Networks and ISDM Systems, Vol. 14, No. 1, pp. 3–24, 1991.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang, “Symbolic Model Checking: 1020 States and Beyond,” Information and Computation, Vol. 98, No. 2, pp. 142–170, June 1992.
J. Callahan, F. Schneider, and S. Easterbrook, “Specification-based Testing Using Model Checking,” in Proceedings of 1996 SPIN Workshop, also Technical Report NASA-IVV-96-022, West Virginia Univeristy, 1996.
E.M. Clarke, E.A. Emerson, and A.P. Sistla, “Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications,” ACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, pp. 244–263, Apr. 1986.
R. Dssouli, K. Saleh, E. Aboulhamid, A. En-Nouaary, and C. Bourhfir, “Test Development for Communication Protocols: towards Automation,” Computer Networks, Vol. 31, Issue 7, pp. 1835–1872, June 1999.
A. Engels, L. Feijs, and S. Mauw, “Test Generation for Intelligent Networks Using Model Checking,” in Proceedings of TACAS’97, Lecture Notes in Computer Science, Vol. 1217, pp. 384–398, Springer-Verlag, 1997.
A. Gargantini and C. Heitmeyer, “Using Model Checking to Generate Tests from Requirements Specifications,” in Proceedings of the Joint 7th European Software Engineering Conference and 7th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 6–10, 1999.
D. Geist, M. Farkas, A. Landver, Y. Lichtenstein, S. Ur, and Y. Wolfsthal, “Coverage-Directed Test Generation Using Symbolic Techniques,” in Proceedings of Formal Methods in Computer Aided Design, 1996.
D. Harel, “Statecharts: a Visual Formalism for Complex Systems,” Science of Computer Programming, Vol. 8, pp. 231–274, 1987.
G.J. Holzmann, “The Model Checker SPIN,” IEEE Transactions on Software Engineering, Vol. 23, No. 5, pp. 279–295, May 1997.
T. Jeron and P. Morel, “Test Generation Derived From Model Checking,” in Computer Aided Verification’ 99, Lecture Notes in Computer Science, Vol. 1633, pp. 108–121, Springer-Verlag, 1999.
R.M. Karp, “Reducibility among Combinatorial Problems,” in Complexity of Computer Computations, R.E. Miller and J.W. Thatcher Eds., Plenum Press, pp. 85–103, 1972.
D. Kozen, “Results on the Propositional Mu-Calculus,” Theoretical Computer Science, Vol. 27, pp. 333–354, 1983.
D. Lee and M. Yannakakis, “Principles and Methods of Testing Finite State Machines—A Survey,” Proceedings of the IEEE, Vol. 84, No. 8, pp. 1090–1123, Aug. 1996.
D. Lee and R. Hao, “Test Sequence Selection,” in Formal Techniques for Networked and Distributed Systems, pp. 269–284, Kluwer Academic Publishers, 2001.
K.L. McMillan, Symbolic Model Checking an Approach to the State Explosion Problem, Kluwer Academic Publishers, 1993.
D. Moundanos, J.A. Abraham, and Y.V. Hoskote, “Abstraction Techniques for Validation Coverage Analysis and Test Generation,” in IEEE Transactions on Computers, Vol. 47, No. 1, pp. 2–14, Jan. 1998.
S. Rapps and E.J. Weyuker, “Selecting Software Test Data Using Data Flow Information,” IEEE Transactions on Software Engineering, Vol. 11, No. 4, pp. 367–375, Apr. 1985.
H. Ural and B. Yang, “A Test Sequence Generation Method for Protocol Testing,” IEEE Transactions on Communications, Vol. 39, No. 4, pp. 514–523, Apr. 1991.
R. de Vries and J. Tretmans, “On-the-Fly Conformance Testing Using SPIN,” International Journal on Software Tools for Technology Transfer, Vol. 2, Issue 4, pp. 382–393, 2000.
M. Weiser, “Program Slicing,” IEEE Transactions on Software Engineering, Vol. 10, No. 4, pp. 352–357, Apr. 1984.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hong, H.S., Lee, I., Sokolsky, O., Ural, H. (2002). A Temporal Logic Based Theory of Test Coverage and Generation. In: Katoen, JP., Stevens, P. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2002. Lecture Notes in Computer Science, vol 2280. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46002-0_23
Download citation
DOI: https://doi.org/10.1007/3-540-46002-0_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43419-1
Online ISBN: 978-3-540-46002-2
eBook Packages: Springer Book Archive