Username   Password       Forgot your password?  Forgot your username? 


Test Scenario Generation using Model Checking

Volume 14, Number 6, June 2018, pp. 1241-1250
DOI: 10.23940/ijpe.18.06.p15.12411250

Zhixiong Yina, Min Zhangb, Guoqiang Lic, and Ling Fangd

aSchool of Engineering Sciences, University of Chinese Academy of Sciences, Beijing, 100049, China
bShanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, 200062, China
cSchool of Software, Shanghai Jiao Tong University, Shanghai, 200240, China
dInstitute of Technology Innovation, Hefei Institutes of Physical Science, Chinese Academy of Sciences, Hefei, 230031, China

(Submitted on March 17, 2018; Revised on April 14, 2018; Accepted on May 21, 2018)


Testing, including designation, execution and bug analysis has been broadly adopted in various industries. Test cases must be designed to confirm the entire behavior of the object system. In practice, a test case normally includes a series of operations that cold conduct the system status eventually to fulfill the precondition of the targeted test case. However, the applications to trigger the function calls of the software system would often be manually composed in traditional test activities, which is difficult especially for complex concurrent systems. Insufficient testing might result in hidden system defects, which increases the likelihood of economic loss or human injury. Model checking is a formal technique that can check the properties of a system automatically with strictness, completeness, and traceability. In this paper, a novel formal approach is proposed to systematically generate test scenarios automatically with traceability by the model checking technique. Meanwhile, the scenarios are reliable and precise, and debugging also becomes easier. Moreover, despite the reduction in demand of an experienced test engineer to design the target test cases, the coverage could be improved as the tedious and complicated processes of test scenario generation are accomplished by the model checker. This method has been applied in two practical case studies, and the results show the effectiveness of the proposed approach in terms of high coverage, automation, traceability and reusability.


References: 18

        1. F. Abbors, and D. Truscan. “Approaching Performance Testing from a Model-Based Testing Perspective”, Proceedings of the 2th International Conference on Advances in System Testing and Validation Lifecycle (VALID), pp.125–28, 2010.
        2. C. Baier, and J. P. Katoen. “Principles of Model Checking”. Publisher: The MIT Press, ISBN-10: 026202649, 2008.
        3. T. Ball, and S. K. Rajamani. “SLIC: A Specification Language for Interface Checking”. Technical Report, MSR-TR-2001-21, Microsoft Research, 2002.
        4. B. Beizer. “Software Testing Technologies”. ISBN: 1850328803, Publisher: Itp-Media, 2nd Edition 1990.
        5. E. M. Clarke, O. Grumberg, and D. A. Peled. “Model Checking”, Publisher: MIT Press, ISBN: 9780262032704, 2000.
        6. M. Daum, N. W. Schirmer and M. Schmidt. “Implementation Correctness of a Real-time Operating System”. Proceedings of the 7th IEEE International Conference on Software Engineering and Formal Methods. IEEE Computer Society, pp.23–27, 2009.
        7. G. Fraser, F. Wotawa, and P. E. Ammann. “Testing with Model Checkers: A survey”. SNA Technical Report, 2007.
        8. L. Fang, T. Kitamura, T. B. N. Do, and H. Ohsaki. “Formal Model-Based Test for AUTOSAR Multicore RTOS”. Proceedings of the 5th IEEE International Conference on Software Testing, Verification and Validation. IEEE Computer Society, pp.251–259, 2012.
        9. J. M. Glenford. “The Art of Software Testing”. Publisher: Wiley, ISBN: 0471469122, 2004.
        10. G. Hamon, L. D. Moura, and J. Rushby. “Generating Efficient Test Sets with a Model Checker”. Proceedings of the 2th IEEE International Conference on Software Engineering and Formal Methods, IEEE Computer Society, pp.261–270, 2007.
        11. M. P. Heimdahl, S. Rayadurgam, W. Visser, G. Devaraj, and J. Gao. “Auto-generating Test Sequences Using Model Checkers: A Case Study”. Proceedings of the 3th International Workshop Formal Approaches to Software Testing. Springer, LNCS 2931, pp.42–59, 2004.
        12. G. J. Holzmann. “The Model Checker SPIN. IEEE Transactions on Software Engineering”. Vol. 30, No. 6, pp.626–634, 1989.
        13. Q. Li, and C. Yao, “Real-time Concepts for Embedded Systems”, CMP Press, 2003.
        14. B. Lindstrom, P. Pettersson, and J. Offutt. “Generating Trace-Sets for Model-based Testing”. Proceedings of the 18th IEEE International Symposium on Software Reliability Engineering. IEEE Computer Society, pp.171–180, 2007.
        15. OSEK test plan:
        16. SpecExplore homepage:
        17. Toppers homepage:
        18. Zipc homepage (in Japanese): tester.pdf.


              Please note : You will need Adobe Acrobat viewer to view the full articles.Get Free Adobe Reader

              Download this file (IJPE-2018-06-15.pdf)IJPE-2018-06-15.pdf[Test Scenario Generation using Model Checking]807 Kb
              This site uses encryption for transmitting your passwords.