A Formal Method for Testing Reactive System from Symbolic Model

详细信息    查看全文

• 作者：Yongbing Wan (1) wybingsh@163.com
  Zhongwei Xu (1) xuzhongweish@163.com
  Meng Mei (1) mei_meng@163.com
• 关键词：symbolic model – ; conformance testing – ; symbolic execution – ; test case generation
• 刊名：Lecture Notes in Computer Science
• 出版年：2012
• 出版时间：2012
• 年：2012
• 卷：7530
• 期：1
• 页码：612-625
• 全文大小：341.8 KB
• 参考文献：1. Manna, Z., Pnueli, A.: Temporal verification of reactive systems: safety. Springer-Verlag, New York, Inc. (1995)
  2. 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)
  3. 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)
  4. 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)
  5. 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)
  6. Shuhao, L., Ji, W., Wei, D.: A Framework of Property-Oriented Testing of Reactive Systems. Acta Electronica Sinica 32, 222–225 (2004)
  7. Rusu, V.: Combining Formal Verification and Conformance Testing for Validation Reactive System. Software Testing, Verification and Reliability 13(3), 157–180 (2003)
  8. 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)
  9. 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)
  10. 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)
  11. 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)
  12. 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)
  13. 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)
  14. 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)
  15. 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)
  16. 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)
  17. Ahmed, K.: Complete Test Graph Synthesis for Symbolic Real-time Systems. Electronic Notes in Theoretical Computer Science, 79–100 (2003)
  18. Tretmans, J., Brinksma, E.: TroX: automated model-based testing. In: Proc. First European Conference on Model-Driven Software Engineering, pp. 31–43 (2003)
  19. Simao, A., Petrenko, A.: Generating asynchronous test cases from test purposes. Information and Software Technology, 1252–1262 (2011)
  20. Thierry, J.: Symbolic Model-based Test Selection. Electronic Notes in Theoretical Computer Science, 167–184 (2009)
  21. 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)
• 作者单位：1. School of Electronics & Information Engineering, Tongji University, Shanghai, China
• ISSN：1611-3349

文摘

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.