不論是軟體專案、工程專案或是其他許許多多的應用程式，在完成之前總是需要大大小小的測試來驗證其可靠性。以軟體來說單元測試、功能測試接著是整合測試等等。但是測試所花費的成本十分的高，不管是人力成本或是其他相關的軟硬體成本都不少。而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.

[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