簡易檢索 / 詳目顯示

研究生: 林劭彥
Shao-Yan Lin
論文名稱: 對於非決定性並行軟體的語句覆蓋測試
Statement Coverage Testing for Non-deterministic Concurrent Software
指導教授: 黃冠寰
Hwang, Gwan-Hwan
學位類別: 碩士
Master
系所名稱: 資訊工程學系
Department of Computer Science and Information Engineering
論文出版年: 2010
畢業學年度: 98
語文別: 中文
論文頁數: 63
中文關鍵詞: 並行程式符號執行可達性測試語句覆蓋
英文關鍵詞: current program, symbolic execution, Reachability Testing, statement coverage
論文種類: 學術論文
相關次數: 點閱:117下載:1
分享至:
查詢本校圖書館目錄 查詢臺灣博碩士論文知識加值系統 勘誤回報
  • 不論是軟體專案、工程專案或是其他許許多多的應用程式,在完成之前總是需要大大小小的測試來驗證其可靠性。以軟體來說單元測試、功能測試接著是整合測試等等。但是測試所花費的成本十分的高,不管是人力成本或是其他相關的軟硬體成本都不少。而statement coverage通常被要求是軟體測試中的一項指標。
    在並行程式中的statement coverage需要考慮數隻程式同時執行的情況,如何得知有哪些statement無法執行到是因為什麼條件,便需要利用symbolic execution。再來同一組輸入執行多次可能有不同的結果,要如何將所有的可能的interleaving都一一找到,這邊介紹了三種方法Concolic Testing、Model checking與Reachability Testing並加以介紹與比較。
    此篇研究主要在於發展一種測試的方法,來達到statement coverage。以現有的Reachability Testing為基礎,加上symbolic execution來達成statement coverage。提出一套演算法利用Statement Mapping Table來和SYN-sequence結合,來探討程式中未能執行到的statement是否可透過更改輸入,來讓它被執行到。最後告知使用者程式是否有存在dead code無法執行到或是可以在一個或數個輸入之下順利達成statement coverage。

    No matter what the software project, engineering projects or other applications is, we need a lot of different tests to verify the reliability before completion.In software testing, we need unit testing first, and then function testing. Finally, we need to integration testing. But the cost of testing is extremely high, regardless of human cost, or other related costs. And Statement Coverage is usually a criterion of software testing.Statement coverage in concurrent software needs to consider the different application execution simultaneously. To know which statement cannot be performed and with what condition, we need to use symbolic execution. Because the same input might causes different results, we should find out all the possible interleaving.
    In this paper, we introduce and compare Concolic Testing, Model checking and Reachability Testing.The purpose in this paper is to develop a testing method to achieve the Statement Coverage.In addition to achieve Statement Coverage, we combine existing Reachability Testing and symbolic execution together . We propose an algorithm which uses the Statement Mapping Table with the SYN-sequence to discuss whether the non-reach statement can be executed by changing the input. Last but not the less, we would tell the user whether the program exists dead code cannot be performed or can enter in one or several inputs to reach Statement coverage.

    附表目錄 Ⅵ 附圖目錄 VII 第一章 簡介 1 1.1 CONCURRENT PROGRAM 1 1.2 STATEMENT COVERAGE TESTING 2 1.3 DIFFERENT WAY TO PERFORM STATEMENT COVERAGE TESTING FOR CONCURRENT PROGRAM 4 第二章 文獻探討 6 2.1 SYMBOLIC EXECUTION 6 2.2 CONCOLIC TESTING 8 2.3 MODEL CHECK 10 2.4 REACHABILITY TESTING 12 第三章 REACHABILITY TESTING與SYMBOLIC EXECUTION來達成STATEMENT COVERAGE 15 3.1 A-SET RULE 16 3.2 STATEMENT MAPPING TABLE 18 3.3 TRY_1_ ALGORITHM 22 3.4 TOTAL ORDER 26 3.5 PERFORM TRY_1_ ALGORITHM 32 3.6 TRY_2_ ALGORITHM 37 3.7 PERFORM TRY_2_ ALGORITHM 39 3.8 PROOF 50 第四章 實作比較與實驗結果 53 4.1 ALGORITHM實作與比較應用於圖 3. 2範例 53 4.2 ALGORITHM實作與比較應用於範例二 56 第五章 結論和展望 59 5.1 結論 59 5.2 展望 59 參考文獻 61

    [1] Charles E. Mcdowell and David P. Helmold, “Debugging Concurrent
    Programs,” ACM Computing Surveys, Volume 21, Issue 4, December 1989.
    [2] K.C. Tai and Richard H. Carver, “Testing of Distributed Programs,” Chapter 33
    in Parallel and Distributed Computing Handbook, Editor: A. Y.
    Zomaya, McGraw-Hill, 1996.
    [3] Anne Dinning, “A Survey of Synchronization Methods for Parallel Computers,”
    IEEE Computer, July 1989.
    [4] Abraham Silberschatz, Peter Baer Galvin, and Greg Gagne, “Operating System
    Concepts,” John Wiley & Sons, ISBN: 0471417432, 6th Edition (June 26,
    2001).
    [5] John Joseph Chilenski and Steven P.Miller, “Applicability of modified
    condition /decision coverage to software testing,” Software Engineering
    Journal, September 1994
    [6] Godefroid, Patrice; Nils Klarlund, Koushik Sen (2005). “DART: Directed
    Automated Random Testing,” Proceedings of the 2005 ACM SIGPLAN
    conference on Programming language design and implementation. New York,
    NY: ACM. pp. 213–223. ISSN 0362-1340. Retrieved 2009-11-9.
    [7] Edmund M. Clarke, “Model checking”, Lecture Notes in Computer Science,
    1997, Volume 1346/1997, 54-56, DOI: 10.1007/BFb0058022
    [8] James C. King, “Symbolic execution and program testing,” Communications of
    the ACM CACM Homepage archive Volume 19 Issue 7, July 1976
    [9] Gwan-Hwan Hwang, “A Systematic Parallel Testing Method for
    Concurrent Programs,” Master Thesis, Institute of Computer
    Science and Information Engineer, National Chiao-Tung University, Taiwan,
    1993.
    [10] Gwan-Hwan Hwang, Kuo-Chung Tai, and Ting-Lu Huang, “Reachability
    Testing: An Approach To Testing Concurrent Software,” International Journal 62

    of Software Engineering and Knowledge Engineering, 5, 4, (Dec. 1995),
    493-510.
    [11] Tao Xie, Darko Marinov, Wolfram Schulte and David Notkin, “Symstra: A
    Framework for Generating Object-Oriented Unit Tests Using Symbolic
    Execution,” Lecture Notes in Computer Science, 2005, Volume 3440/2005,
    365-381, DOI: 10.1007/978-3-540-31980-1_24
    [12] Williams, Nicky; Bruno Marre, Patricia Mouy (2004), “On-the-Fly Generation
    of K-Path Tests for C Functions,” Proceedings of the 19th IEEE International
    Conference on Automated Software Engineering (ASE 2004), 20-25 September
    2004, Linz, Austria. IEEE Computer Society. pp. 290–293. ISBN
    0-7695-2131-2.
    [13] Williams, Nicky; Bruno Marre, Patricia Mouy, Muriel Roger (2005),
    “PathCrawler: Automatic Generation of Path Tests by Combining Static and
    Dynamic Analysis”. Dependable Computing - EDCC-5, 5th European
    Dependable Computing Conference, Budapest, Hungary, April 20-22, 2005,
    Proceedings. Springer. pp. 281–292. ISBN 3-540-25723-3.
    [14] Dawson, Engler, Cristian Cadar, Vijay Ganesh, Peter Pawloski, David L. Dill
    and Dawson Engler (2006), “EXE: Automatically Generating Inputs of Death,”
    Proceedings of the 13th International Conference on Computer and
    Communications Security (CCS 2006). Alexandria, VA, USA: ACM
    [15] Sen, Koushik; Darko Marinov, Gul Agha (2005). “CUTE: a concolic unit
    testing engine for C, ” Proceedings of the 10th European software
    engineering conference held jointly with 13th ACM SIGSOFT international
    symposium on Foundations of software engineering. New York, NY: ACM.
    pp. 263–272. ISBN 1-59593-014-0, Retrieved 2009-11-9.
    [16] Sen, Koushik and Gul Agha (August 2006). “CUTE and jCUTE : Concolic
    Unit Testing and Explicit Path Model-Checking Tools, ” Computer Aided
    Verification: 18th International Conference, CAV 2006, Seattle, WA, USA,
    August 17-20, 2006, Proceedings. Springer. pp. 419–423. ISBN
    978-3-540-37406-0, Retrieved 2009-11-9.,
    [17] G.J. Holzmann. The Model Checker SPIN. IEEE Trans. Soft. Engin., Vol.23,
    No.5, pages 279–295, May 1997.
    [18] J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic model checking: 1020 states and beyond. In IEEE
    Symposium on Logic in ComputerScience, pages 428{439,
    1990}.Pnueli. A temporal logic of concurrent programs.
    Theoretical Computer Science, 13(1):45-60, 1981.
    [19] Honghua Cao, Shi Ying, Dehui Du, Setp. 2006,
    “Towards Model-based Verification of BPEL with Model Checking", IEEE
    International Conference on Computer and Information Technology. pp.
    190-194
    [20] Armin Biere, Alessandro Cimatti, Edmund Clarke and Yunshan Zhu,
    “Symbolic Model Checking without BDDs,” Lecture Notes in Computer
    Science, 1999, Volume 1579/1999, 193-207, DOI: 10.1007/3-540-49059-0_14
    [21] Khurshid, S., Pasareanu, C., Visser, W., “Generalized Symbolic Execution for
    Model Checking and Testing,” In: Garavel, H., Hatcliff, J.(eds.) TACAS 2003.
    LNCS,vol. 2619, pp. 553-568. Springer, Heidelberg(2003)
    [22] Visser, W., Havelund, K., Brat, G., Park, S: “Java PathFinder-second
    generation of a Java model checker,” In: Proc. of Post-CAV Workshop on
    Advance in Verification, Chicago(July 2000)
    [23] Che-Sheng Lin and Gwan-Hwan Hwang, “State-Cover Testing for
    Nondeterministic Terminating Concurrent Programs with an Infinite Number of
    Synchronization Sequences,” Department of Computer Science and
    Information Engineering, National Taiwan Normal University, 11677 Taipei
    City, Taiwan
    [24] Koushik Sen and Gul Agha, “ Automated Systematic Testing of Open
    Distributed Programs,” Lecture Notes in Computer Science, 2006, Volume
    3922/2006, 339-356, DOI: 10.1007/11693017_25
    [25] Frances E. A l l e n, “Control Flow Analysis,” ACM SIGPLAN Notices -
    Proceedings of a symposium on Compiler optimization Homepage archive
    Volume 5 Issue 7, July 1970

    下載圖示
    QR CODE