Abstract
Testing each component in isolation is not always feasible. We consider FSM-based deterministic testing on an Implementation Under Test (IUT) together with some other correctly implemented components as its context. The behavior of the context needs to be taken into account for generating test sequences. We employ model checking tools to retrieve necessary information from the context specification so that a test suite for the IUT integrated with its context can be generated. The use of model checking tools frees us from the necessity of constructing the global model of the IUT and its context, and thus helps avoid the state explosion problem. In the current work, we consider the situations when the context is an embedded system, i.e. it communicates and only communicates with the IUT. In this setting, we present a method to derive a complete test suite that can be used to check for trace pre-order between the FSM representing the integrated implementation of the IUT and its context and the synchronous product of the specification FSM of the IUT and that of its context.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Tretmans, J.: Conformance testing with labelled transition systems: Implementation relation and test generation. Computer Networks and ISDN Systems 29, 49–79 (1996)
Petrenko, A., Yevtushenko, N., von Bochmann, G., Dssouli, R.: Testing in context: framework and test derivation. Computer Communications 19(14), 1236–1249 (1996)
Chow, T.: Testing software design modeled by finite-state machines. IEEE Trans. Software Eng. SE-4(3), 178–187 (1978)
Sabnani, K., Dahbura, A.: A protocol test generation procedure. Computer Networks and ISDN Systems 4(15), 285–297 (1988)
Hennie, F.: Fault detecting experiments for sequential circuits. In: Proc. of 5th Ann. Symp. Switching Circuit Theory and Logical Design, pp. 95–110 (1964)
van der Bijl, M., Rensink, A., Tretmans, J.: Compositional testing with ioco. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 86–100. Springer, Heidelberg (2004)
Hierons, R.M., Ural, H.: UIO sequence based checking sequences for distributed test architectures. Information and Software Technology 45(12), 793–803 (2003)
Chen, J., Hierons, R.M., Ural, H., Yenigun, H.: Eliminating redundant tests in a checking sequence. In: Khendek, F., Dssouli, R. (eds.) TestCom 2005. LNCS, vol. 3502, pp. 146–158. Springer, Heidelberg (2005)
Gonenc, G.: A method for the design of fault detection experiments. IEEE Trans. Computers 19(6), 551–558 (1970)
Ural, H., Wu, X., Zhang, F.: On minimizing the lengths of checking sequences. IEEE Transactions on Computers 46(1), 93–99 (1997)
Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines — a survey. Proceedings of The IEEE 84(8), 1090–1123 (1996)
Holzmann, G.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL - a tool suite for automatic verification of real-time systems. In: Proc. of the DIMACS/SYCON workshop on Hybrid systems III: verification and control: verification and control, pp. 232–243 (1995)
Lima, L.P., Cavalli, A.R.: A progmatic approach to generating test sequences for embedded systems. In: Proc. of 10th International Workshop on Testing of Communicating Systems, pp. 125–140 (1997)
Petrenko, A., Yevtushenko, N., von Bochmann, G.: Fault models for testing in context. In: Proc. of Internation Conference on Formal Techniques for Networked and Distributed Systems, pp. 125–140 (1996)
Petrenko, A., Yevtushenko, N.: Testing faults in embedded components. In: Proc. of 10th International Workshop on Testing of Communicating Systems, pp. 272–287 (1997)
El-Fakih, K., Petrenko, A., Yevtushenko, N.: FSM test translation through context. In: Uyar, M.Ü., Duale, A.Y., Fecko, M.A. (eds.) TestCom 2006. LNCS, vol. 3964, pp. 245–258. Springer, Heidelberg (2006)
El-Fakih, K., Yevtushenko, N.: Fault propagation by equation solving. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 185–198. Springer, Heidelberg (2004)
Robinson-Mallett, C., Liggesmeyer, P., Mcke, T., Goltz, U.: Generating optimal distinguishing sequences with a model checker. ACM SIGSOFT Software Engineering Notes 30(4), 1–7 (2005)
Holzmann, G.: The Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)
Ammann, P.E., Black, P.E., Majurski, W.: Using model checking to generate test from specifications. In: Proc. of 2nd IEEE International Conference on Formal Engineering Methods (ICFEM 1998), pp. 46–54 (1998)
Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. ACM SIGSOFT Software Engineering Notes 24(6), 146–162 (1999)
de Vries, R., Tretmans, J.: On-the-fly conformance testing using Spin. International Journal on Software Tools for Technology Transfer 2(4), 382–393 (2000)
Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: Data flow testing as model checking. In: Proc. of IEEE ICSE 2003, pp. 232–242 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Duan, L., Chen, J. (2008). An Approach to Testing with Embedded Context Using Model Checker. In: Liu, S., Maibaum, T., Araki, K. (eds) Formal Methods and Software Engineering. ICFEM 2008. Lecture Notes in Computer Science, vol 5256. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88194-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-88194-0_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88193-3
Online ISBN: 978-3-540-88194-0
eBook Packages: Computer ScienceComputer Science (R0)