TIAN Cong, LIU Shaoying, DUAN Zhenhua, “Test Case Generation from Conjunctions of Predicates with Model Checking,” Chinese Journal of Electronics, vol. 23, no. 2, pp. 271-277, 2014,
Citation: TIAN Cong, LIU Shaoying, DUAN Zhenhua, “Test Case Generation from Conjunctions of Predicates with Model Checking,” Chinese Journal of Electronics, vol. 23, no. 2, pp. 271-277, 2014,

Test Case Generation from Conjunctions of Predicates with Model Checking

Funds:  This work is supported by the Hosei University HIF Fellowship, the National Natural Science Foundation of China (No.61003078, No.61133001, No.61272117, and No.91218301), the National Basic Research Program of China (973 Program) (No.2010CB328102), ISN Lab (No.ISN1102001).
  • Received Date: 2013-01-01
  • Rev Recd Date: 2013-04-01
  • Publish Date: 2014-04-05
  • Automatic test case generation from a prepost style formal specification must deal with the issue of how to generate test cases from a conjunction of atomic predicate expressions, but unfortunately this problem has not been effectively solved due to its intrinsic difficulty. We describe a practical approach to tackling this problem by utilizing the model checking technique. An algorithm that converts test case generation from a conjunction of atomic predicate expressions into model checking is proposed. We discuss how the algorithm deals with atomic predicate expressions involving only variables of numeric types, and extend the discussion to variables of compound types such as set, sequence, and composite types. Case studies are presented to assess the feasibility and effectiveness of our approach.
  • loading
  • M. Donat, "Automating formal specification-based testing", Proceedings of TAPSOFT'97, Lille, France: Springer-Verlag, pp.833-848, 1997.
    S. Khurshid and D. Marinov, "TestEra: Specification-based testing of Java programs using SAT", Automated Software Engineering, Vol.11, No.4, pp.403-434, 2004.
    M.G. Hinchey and J.P. Bowen (ed.). "Industrial-Strength Formal Methods in Practice", FACIT series. Springer-Verlag, London, UK, 1999.
    J.Woodcock, P.G. Larsen, J. Bicarregui and J. Fitzgerald, "Formal methods: Practice and experience", ACM Computing Surveys, Vol.41, No.4, 2009.
    J. Dick and A. Faivre, "Automating the generation and sequencing of test cases from model-based specifications", Proceedings of FME '93: Industrial-Strength Formal Methods, Odense, Denmark, Vol.670, pp.268-284, 1993.
    S. Liu and S. Nakajima, "A decompositional approach to automatic test case generation based on formal specifications" 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010), pp.147-155, Singapore, 2010.
    M. Utting and B. Legeard, Practical Model-Based Testing: A Tools Approach, Morgan Kaufmann, 2007.
    Gerard J. Holzmann, "The model checker spin", IEEE Trans. on Software Engineering, Vol.23, No.5, pp.279-295, 1997.
    E.M. Clarke and E.A. Emerson, "Desigh and syntesis of synchronization skeletons using branching time temporal logic", Logic of Programs 81, LNCS 131, Springer, pp.52-71, 1981.
    J.P. Quielle and J. Sifakis, "Specification and verification of concurrent systems in CESAR", Proceedings of the 5th International Symposium on Programming, pp.337-350, 1981.
    A. Pnueli, "The temporal logic of programs", Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, IEEE, New York, pp.46-67, 1977.
    Markus Müller-Olm, David Schmidt and Bernhard Steffen, "Model-checking a tutorial introduction", Proceedings of SAS'99, LNCS 1694, pp.330-354, 1999.
    Gerard J. Holzmann, The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley, ISBN 0-321-22862-6, 2003.
    S. Liu and S. Nakajima, "A "Vibration" method for automatically generating test cases based on formal specifications", APSECC 2011, pp.73-80, 2011.
    J. Callahan, F. Schneider and S. Eastbrook, "Specificationbased testing using model-checking", Proc. 2nd SPIN Workshop, pp.193-207, 1996.
    Hamon, L. de Moura and J. Rushby, "Automated test generation with SAL", CSL Technical Note, 2005.
    D. Jackson, Software Abstractions, The MIT Press, 2006.
    B. Dutertre and L. de Moura, "The YICES SMT Solver", http://yices.csl.sri.com/.
    H. Lin and W. Zhang, "Model checking: Theories, techniques and applications", Acta Electronica Sinica, Vol.30, No.12A, pp.1907-1912, 2002.
    C. Zhou, Z. Tao, D. Ding and L. Wang, "Bounded model checking for branching-time temporal logic", Chinese Journal of Electronics, Vol.15, No.4, pp.675-678, 2006.
  • 加载中


    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Article Metrics

    Article views (571) PDF downloads(1253) Cited by()
    Proportional views


    DownLoad:  Full-Size Img  PowerPoint