並行程式面臨非確定行為的問題：在相同的輸入下重複執行多次可能產生不同的同步事件序列和執行結果。這使得並行程式難以進行測試。對非確定行為的並行程式進行動態測試的常見方法是將受測的並行程式重複執行許多次。每次執行受測的並行程式會產生一個同步序列（SYN-sequences）。除了執行結果之外，我們通常還必須驗證搜集到的SYN-sequences以確保並行程式的行為滿足我們所要求的規格或需求。這篇論文的目標即在於驗證SYN-sequences。
我們提出了對SYN-sequence進行正規驗證的方法。首先，我們研究用以驗證SYN-sequences的規格或需求的表達法。根據SYN-sequence表達了同步事件間偏序關係的事實，我們採用temporal logic來表示規格。接下來的目標就是如何有效率的根據規格來驗證SYN-sequences。因此，我們發展了三種不同的方法來將SYN-sequence轉換成模型，然後就可以利用temporal logic做正規驗證。我們也探討了如何用適當的表達法表達規格，以及如何選擇合適的模型。實驗結果驗證了對SYN-sequence進行有效率的驗證是可行的。

Concurrent programs exhibit nondeterministic behavior in that multiple executions thereof with the same input might produce different sequences of synchronization events and different results. It makes the concurrent programs difficult to test. Dynamic testing of a concurrent program with nondeterministic behavior usually involves multiple executions of the target concurrent program. Each execution of the target concurrent program produces a synchronization sequences or SYN-sequences. In addition to the execution results, we usually have to verify the collected SYN-sequences to make sure that the behavior of the concurrent program meets its specification or requirement. In this thesis, we target on how to verify the SYN-sequences.
We propose a scheme for the formal verification of the SYN-sequence. First, we study how to express the specification or requirement which can be used to verify SYN-sequences. According to the fact that a SYN-sequence represents a partial order relationship of synchronization events, we employ the temporal logic to express the specification. Then, we target on how to efficiently verify SYN-sequences according to the specification. As a result, we develop three different methods to transfer the target SYN-sequence to models which can then be verified in temporal logic. We also discussed how to express the specifications in suitable expression types and how to choose an appropriate model. The experimental results show that a systematic verification of SYN-sequence is feasible.

[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] D. Helmbold and D. Luckham, “Debugging Ada tasking programs,” IEEE Software, Volume 2, Number 2, 66-74, 1985.
[6] K. C. Tai, “Testing of concurrent software,” Proc. of the 13th Annual International Computer Software and Applications Conference, pp. 62-64, 1989.
[7] Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, Model Checking, MIT Press, 1999, ISBN 0-262-03270-8.
[8] Logic in Computer Science: Modelling and Reasoning About Systems, Michael Huth and Mark Ryan, Cambridge University Press, 2004.
[9] Holzmann, G.: The model checker SPIN. IEEE Trans. Software Engineering 23(5) (1997) 279–295
[10] Musuvathi, M., Park, D., Chou, A., Engler, D., L. Dill, D.: CMC: A pragmatic approach to model checking real code. In: OSDI 02: Operating Systems Design and Implementation (2002) 75–88
[11] Java PathFinder, http://javapathfinder.sourceforge.net/.
[12] MAGIC website, http://www.cs.cmu.edu/~chaki/magic.
[13] S. Chaki, J. Ouaknine, K. Yorav, and E. M. Clarke, “Automated compositional abstraction refinement for concurrent C programs,” In Proceedings of SoftMC 03. ENTCS 89(3), 2003.
[14] W. Richards Adrion, Martha A. Branstad, and John C. Cherniavsky, “Validation, Verification, and Testing of Computer Software,” ACM Computing Surveys, Volume 14, Issue 2, June 1982.
[15] Roger S. Pressman, Software Engineering (A practitioner's approach), 5th edition, 2000, Mc Graw-Hill Education, ISBN 978-0071181822.
[16] 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.
[17] G. H. Hwang, K. C. Tai, and T.L. Huang, “Reachability Testing: An Approach To Testing Concurrent Software,” International Journal of Software Engineering and Knowledge Eng., 5, 4, (Dec. 1995), 493-510.
[18] Gwan-Hwan Hwang and Che-Sheng Lin, “Dynamic Effective Testing: An Approach to Testing Concurrent Programs,” Technical Report, National Taiwan Normal University, 2008. http://www.csie.ntnu.edu.tw/~ghhwang/ DET2008.pdf.
[19] Thomas J. LeBlanc and John M. Mellor-Crummey, “Debugging Parallel Programs with Instant Replay,” IEEE Transactions on Computers, C-36(4), pp. 471-482, April 1987.
[20] Che-Sheng Lin and Gwan-Hwan Hwang, “Dynamic Termination Decision for Concurrent Programs with Busy-Waiting Loops,” Submitted to IEEE International Conference on Software Testing, Verification, and Validation, 2009 for publication.
[21] NuSMV, http://nusmv.irst.itc.it/.
[22] Stoller SD. Testing concurrent Java programs using randomized scheduling. Proceedings of the 2nd Workshop on Runtime Verification (RV) (Electronic Notes in Theoretical Computer Science, vol. 70(4)). Elsevier: Amsterdam, 2002.
[23] Y. Ben-Asher, E. Farchi, Y. Eytani, “Heuristics for finding concurrent bugs,” Proceedings of the International Parallel and Distributed Processing Symposium (IPDPS 2003) PADTAD Workshop, April 2003. IEEE Computer Society Press: Los Alamitos, CA, 2003. Edelstein O, Farchi E, Nir Y, Ratsaby G, Ur S. Multithreaded Java program test generation. IBM Systems Journal 2002; 41(1):111–125. Available at: http://www.research.ibm.com/journal/sj/411/edelstein.html.
[24] Gwan-Hwan Hwang, Sheng-Jen Chang, and Huey-Der Chu, “Technology for Testing Nondeterministic Client/Server Database Applications,” IEEE Transaction on Software Engineering, Volume 30, Number 1, pp. 59-77, Jan., 2004.
[25] Kuo-Chung Tai, “Reachability Testing of Asynchronous Message-passing Programs,” Proceedings of the second International Workshop on Software Engineering for Parallel and Distributed Systems, 1997.
[26] Yu Lei and Kuo-Chung Tai, “Efficient Reachability Testing of Asynchronous Message-Passing Programs,” Proc. 8th IEEE Intl. Conf. on Engineering for Complex Computer Systems, pp. 35-44, Dec. 2002.
[27] Richard H. Carver and Yu Lei, “A General Model for Reachability Testing of Concurrent Programs,” ICFEM 2004, LNCS 3308, pp. 76-89, 2004.
[28] Yu Lei and Richard H. Carver, “Reachability Testing of Concurrent Programs,” IEEE Transaction on Software Engineering, June 2006 (Vol. 32, No. 6), pp. 382-403.
[29] Yu Lei, Richard H. Carver, Raghu Kacker, and David Kung, “A combinatorial testing strategy for concurrent programs,” Software Testing, Verification & Reliability ,Volume 17 , Issue 4 (December 2007) pages 207-225.
[30] Koushik Sen, Gul Agha, “Automated Systematic Testing of Open Distributed Programs,” Fundamental Approaches to Software Engineering, 9th International Conference, FASE 2006, pp. 339-356.
[31] Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. on Foundations of Computer Science. (1977) 46–57
[32] N. Rescher, A.U.: Temporal Logic. Springer (1971)
[33] Goldblatt, R.: Logic of time and computation. Technical report, CSLI Lecture Notes, no.7, Stanford University (1987)
[34] Kamp, J.: Tense Logic and the Theory of Order. PhD thesis, UCLA (1968)
[35] Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Logics of Programs. Volume 193 of Lecture Notes in Computer Science., Springer (1985) 196–218
[36] Markey, N.: Temporal logic with past is exponentially more succinct. EATCS Bulletin 79 (2003) 122–128
[37] Vardi, M.: A temporal fixpoint calculus. In: Proc. 15th ACM Symp. on Principles of Programming Languages. (1988) 250–259
[38] Keller, R.: Formal verification of parallel programs. Communications of the ACM 19 (1976) 371–384
[39] Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press (2002)
[40] Pratt, V.: A near-optimal method for reasoning about action. Journal of Computer and Systems Science 20(2) (1980) 231–254
[41] Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proc. Workshop on Logic of Programs. Volume 131 of Lecture Notes in Computer Science., Springer (1981) 52–71
[42] Queille, J., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Proc. 9th ACM Symp. on Principles of Programming Languages. Volume 137 of Lecture Notes in Computer Science., Springer (1982) 337–351
[43] Ben-Ari, M., Manna, Z., Pnueli, A.: The logic of nexttime. In: Proc. 8th ACM Symp. on Principles of Programming Languages. (1981) 164–176
[44] Lamport, L.: “Sometimes” is sometimes “not never” - on the temporal logic of programs. In: Proc. 7th ACM Symp. on Principles of Programming Languages. (1980) 174–185
[45] Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In: Proc. 10th ACM Symp. on Principles of Programming Languages. (1983) 117–126
[46] Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languagues and Systems 8(2) (1986) 244–263
[47] Clarke, E., Grumberg, O.: Avoiding the state explosion problem in temporal logic model-checking algorithms. In: Proc. 16th ACM Symp. on Principles of Distributed Computing. (1987) 294–303
[48] Browne, M., Clarke, E., Dill, D., Mishra, B.: Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computing C-35 (1986) 1035–1044
[49] Clarke, E., Mishra, B.: Hierarchical verification of asynchronous circuits using temporal logic. Theoretical Computer Science 38 (1985) 269–291
[50] Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: 10^20 states and beyond. In: Proc. 5th IEEE Symp. on Logic in Computer Science. (1990) 428–439
[51] Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: 10^20 states and beyond. Information and Computation 98(2) (1992) 142–170
[52] McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers (1993)
[53] Clarke, E.: The birth of model checking. In: 25 Years of Model Checking. Volume 5000 of Lecture Notes in Computer Science., Springer (2008) 1–26
[54] Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proc. 12th ACM Symp. on Principles of Programming Languages. (1985) 97–107
[55] CADP, http://www.inrialpes.fr/vasy/cadp/
[56] CHESS, http://research.microsoft.com/en-us/projects/CHESS/.
[57] ISP (In-situ Partial Order), http://www.cs.utah.edu/formal_verification/ISP-release/
[58] Spin – Formal Verification, http://spinroot.com/spin/whatispin.html
[59] Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Computer Aided Verification. Volume 2404 of Lecture Notes in Computer Science., Springer (2002) 241–268
[60] H.Carver, R., Tai, K.-C.: Modern multithreading. John Wiley & Sons (2006)
[61] Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng, SE.3, 7 (1977) 125–143.
[62] Cavada, R., Cimatti, A., A. Jochim, C., Keighren, G., Olivetti, E., Pistore, M., Roveri, M., Tchaltsev, A.: NuSMV 2.4 User Manual. ITC-irst (2005)
[63] Godefroid, P.: Model Checking for Programming Languages using VeriSoft. In: Proc. 24th ACM Symp. on Principles of Programming Languages. (1997) 174–186