Modeling and testing embedded system by model checking

被引：0

作者：

Sun, Fuzhen ^{[1
,2
]}

Song, Dandan ^{[1
]}

Liao, Lejian ^{[1
]}

Li, Guoqiang ^{[1
]}

机构：

[1] Beijing Engg. Res. Centre of High Volume Language Information Processing and Cloud Computing Appl, Beijing Key Laboratory of Intelligent Information Technology, School of Computer Science, Beijing Institute of Technology

[2] School of Computer Science and Technology, Shandong University of Technology

来源：

International Journal of Advancements in Computing Technology | 2012年 / 4卷 / 17期

关键词：

Automatic testing; Model checking; Test case generation; Timed automata;

D O I：

10.4156/ijact.vol4.issue17.3

中图分类号：

学科分类号：

摘要：

Software testing is the key validation technique used by industry up to today, but remain error prone and expensive cost. Automatically generating test cases from formal models of the system under test is a promising improvement approach to cut down the testing cost. This paper introduces a technique that automatically generate real-time conformance test cases from timed automata specifications. First, both reactive system and its environment is modeled by restricted automata with the notion of deterministic, input enabled and output urgent. Then demonstration is given to show how to efficiently generate real-time test cases with optimal execution time from diagnostic trace. Finally, we formally specify user's single purpose or coverage criteria to convert the test case generation problem into a reachability problem. This approach is implemented using model checkers as test case generation tools and experiment results on three different coverage criteria specifications show feasibility and effectiveness of our technique.

引用

页码：18 / 27

页数：9

共 20 条

[1]

Fraser G., Wotawa F., Using LTL Rewriting to Improve the Performance of Model-Checker Based Test-Case Generation, AMOST '07: Proceedings of the 3rd International Workshop on Advances in Model-based Testing, pp. 64-74, (2007)

[2]

Calvagna A., Gargantini A., A Logic-Based Approach to Combinatorial Testing with Constraints, Tests and Proofs, pp. 66-83, (2008)

[3]

Jones J.A., Harrold M.J., Test-suite reduction and prioritization for modified condition/decision coverage, IEEE Trans. Softw. Eng, 29, 3, pp. 195-209, (2003)

[4]

Aho A.V., Dahbura A.T., Lee D., Yar M.U., An Optimization Technique for Protocol Conformance Test Generation Based on UIO Sequences and Rural Chinese Postman Tours, IEEE Transactions on Communications, 39, 11, pp. 1604-1615, (1991)

[5]

Bozga M., Fernandez J.-C., Ghirvu L., Jard C., Jeron T., Kerbrat A., Morel P., Mounier L., Verification and Test Generation for the SSCOP Protocol, Science of Computer Programming, 36, 1, pp. 27-52, (2000)

[6]

Bosscher D., Polak I., Vaandrager F., Verification of an Audio-Control Protocol, Proc. of Formal Techniques in Real-Time and Fault-Tolerant Systems, (1994)

[7]

Cardell-Oliver R., Conformance Testing of Real-Time Systems with Timed Automata, Formal Aspects of Computing, 12, 5, pp. 350-371, (2010)

[8]

En-Nouaary A., Dssouli R., Khendek F., Elqortobi A., Timed Test Cases Generation Based on State Characterization Technique, In 19th IEEE Real-Time Systems Symposium (RTSS'98), pp. 220-229, (1998)

[9]

Khoumsi A., A method for testing the conformance of realtime systems, Olderog, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems: 7th International Symposium, FTRTFT 2002, pp. 198-235, (2002)

[10]

Nielsen B., Skou A., Automated test generation from timed automata, International Journal on Software Tools for Technology Transfer, 5, pp. 59-77, (2003)

← 1 2 →