Abstract
Testing is one of the most well-established techniques for the verification and validation of systems. Since success or failure verdicts are emitted with respect to the test case execution results, proper test case selection activities need to be performed. In this paper, we propose an approach to address the problem of generating symbolic test cases to test whether an implementation conforms to its specification, given in terms of reactive systems. This approach is based on a unified symbolic semantic model which can unify data operation and abstract behavior. We adapt the sioco conformance relation to deal with this symbolic model, and then describe a test case generation process, as well as a symbolic execution algorithm based on on-the-fly strategy. The approach has been illustrated on a simple example while the soundness and completeness of the symbolic notions is demonstrated.
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.
Similar content being viewed by others
References
Manna, Z., Pnueli, A.: Temporal verification of reactive systems: safety. Springer-Verlag, New York, Inc. (1995)
Constant, C., Thierry, J., Marchand, H.: Integration Formal Verification and Conformance Testing for Reactive System. IEEE Transactions on Software Engineering 33(8), 558–574 (2007)
Frantzen, L., Tretmans, J., Willemse, T.A.C.: Test Generation Based on Symbolic Specifications. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 1–15. Springer, Heidelberg (2005)
Frantzen, L., Tretmans, J., Willemse, T.A.C.: A Symbolic Framework for Model-Based Testing. In: Havelund, K., Núñez, M., Roşu, G., Wolff, B. (eds.) FATES 2006 and RV 2006. LNCS, vol. 4262, pp. 40–54. Springer, Heidelberg (2006)
Tretmans, J.: Model Based Testing with Labelled Transition Systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 1–38. Springer, Heidelberg (2008)
Shuhao, L., Ji, W., Wei, D.: A Framework of Property-Oriented Testing of Reactive Systems. Acta Electronica Sinica 32, 222–225 (2004)
Rusu, V.: Combining Formal Verification and Conformance Testing for Validation Reactive System. Software Testing, Verification and Reliability 13(3), 157–180 (2003)
Wilkerson, L., Patricia, D.L.: Modeling and Testing Interruptions in Reactive System Using Symbolic Models. In: Proc. of the 2nd Brazilian Workshop on Systematic and Automated Software Testing, pp. 34–43 (2009)
Gaston, C., Le Gall, P., Rapin, N., Touil, A.: Symbolic Execution Techniques for Test Purpose Definition. In: Uyar, M.Ü., Duale, A.Y., Fecko, M.A. (eds.) TestCom 2006. LNCS, vol. 3964, pp. 1–18. Springer, Heidelberg (2006)
Tretmans, J.: Testing Concurrent Systems: A Formal Approach. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 46–65. Springer, Heidelberg (1999)
Claude, J., Thierry, J.: TGV : theory, principles and algorithms: A Tool for the Automatic Synthesis of Conformance Test Cases for Non-Deterministic Reactive Systems. Software Tools for Technology Transfer 7(4), 297–315 (2002)
Clarke, D., Jéron, T., Rusu, V., Zinovieva, E.: STG: A Symbolic Test Generation Tool. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 470–475. Springer, Heidelberg (2002)
Koopman, P., Plasmeijer, R.: Testing Reactive System with GAST. In: Gilmore, S. (ed.) Trends in Functional Programming. Trends in Functional Programming, vol. 4, pp. 111–129 (2003)
Cartaxo, E.G., Andrade, W.L., Neto, F.G.O.: LTSBT: A tool to generate and select functional test cases for embedded systems. In: Proceedings of the 2008 ACM Symposium on Applied Computing, vol. 2, pp. 1540–1544 (2008)
Li, S., Ji, W., Wei, D.: Property-oriented testing of real-time system. In: Proc. of the 11th Asia-Pacific Software Engineering Conference, pp. 358–365. IEEE Computer Society (2004)
Andrade, W.L., Machado, P.D.L.: Interruption Testing of Reactive Systems. In: Oliveira, M.V.M., Woodcock, J. (eds.) SBMF 2009. LNCS, vol. 5902, pp. 37–53. Springer, Heidelberg (2009)
Ahmed, K.: Complete Test Graph Synthesis for Symbolic Real-time Systems. Electronic Notes in Theoretical Computer Science, 79–100 (2003)
Tretmans, J., Brinksma, E.: TroX: automated model-based testing. In: Proc. First European Conference on Model-Driven Software Engineering, pp. 31–43 (2003)
Simao, A., Petrenko, A.: Generating asynchronous test cases from test purposes. Information and Software Technology, 1252–1262 (2011)
Thierry, J.: Symbolic Model-based Test Selection. Electronic Notes in Theoretical Computer Science, 167–184 (2009)
Jéron, T., Morel, P.: Test Generation Derived from Model-Checking. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 108–121. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wan, Y., Xu, Z., Mei, M. (2012). A Formal Method for Testing Reactive System from Symbolic Model. In: Lei, J., Wang, F.L., Deng, H., Miao, D. (eds) Artificial Intelligence and Computational Intelligence. AICI 2012. Lecture Notes in Computer Science(), vol 7530. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33478-8_76
Download citation
DOI: https://doi.org/10.1007/978-3-642-33478-8_76
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33477-1
Online ISBN: 978-3-642-33478-8
eBook Packages: Computer ScienceComputer Science (R0)