對動態測試產生的同步序列之正規驗證的研究

The Formal Verification of SYN-Sequences Generated in Dynamic Testing

李彥佑(Yan-You Li)

指導教授 ： 黃冠寰

國立臺灣師範大學/理學院/資訊工程研究所/碩士(2009年)

摘要

並行程式面臨非確定行為的問題：在相同的輸入下重複執行多次可能產生不同的同步事件序列和執行結果。這使得並行程式難以進行測試。對非確定行為的並行程式進行動態測試的常見方法是將受測的並行程式重複執行許多次。每次執行受測的並行程式會產生一個同步序列（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.

並列關鍵字

dynamic testing ； reachability testing ； formal verification ； model checking ； SYN-sequence

參考文獻

[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.

[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.

[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.

[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

[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.