臺灣博碩士論文加值系統

模型檢測(model checking)技術在最近幾年發展越來越成熟，然而在實際上不容易將這技術應用在軟體，特別是要直接從原始碼抽出模型，原因在於軟體會產生的狀態(state)多於硬體。此外，要如何確保從模型到實作的差距也是個困難的議題。
本篇論文中，我們使用幾個例子來說明：當一個程序(process)含有複雜的陣列(array)行為時「模型的實作選擇會造成在分析時有很大的影響」。換句話說，軟體驗證(software verification)的結果跟模型的實作選擇有很大的關係。為了減少模型實作選擇的影響力，我們建議在模型描述語言(model description language)提供抽象的資料型別(abstract data type)，並且避免使用讓使用者用陣列來實作這些抽象資料型別。鼓勵使用這些抽象資料型別除了可以減少在驗證時模型實作選擇的影響力，我們也可以使用作適合該資料型別的分析方式。
我們實作了COCOV(Compositional Concurrency Verifier)，以rc-Promela(修改自Promela，Promela是驗證工具SPIN的模型描述語言)為基礎並且讓COCOV支援了set、queue的抽象資料型別，並說明如何透過該工具讓我們可以在分析時獲得明顯的幫助，尤其是在局部性分析(compositional analysis)與我們的refactoring技術。

Model Checking techniques have improved considerably in past decades. In practice, there are some difficulties to apply model checking technology to software, particularly to source code directly. Not only software has more states, but also it is not easy to narrow the gap between an implementation and its model. One of the problems is how to deal with the abstract data type in source code. In this thesis we present examples to show different modeling choices can result in great differences in analysis when process behaviors are complicated by array data type. In other words, software verification is very sensitive to modeling choices. To lessen the sensitivity, we advocated the support of abstract data types in model description languages and suppressing the use of array. Encouraging the use of abstract data types can lessen the sensitivity of analysis to modeling choices and converge the process behaviors to their best for analysis.
In this work, we implement a tool named COCOV (Compositional Concurrency Verifier) supports abstract data types. We show that analysis (particularly, compositional analysis and our refactoring technique) can benefit from this tool support in an obvious way.

CHAPTER 1 INTRODUCTION 1
1.1 Overview 1
1.2 Organization 6
CHAPTER 2 BACKGROUND 7
2.1 Model checking 7
2.2 Communication finite state machine (CFSM) 8
2.3 Promela and rc-Promela 9
2.4 Model checking tools 12
2.5 Related software verification tools 13
2.6 Compositional analysis 14
2.7 Model Refactoring 17
CHAPTER 3 HOW SOFTWARE ANALYSIS IS SENSITIVE TO MODELING CHOICES 20
CHAPTER 4 IMPLEMENTATION OF ABSTRACT DATA TYPE IN COCOV 32
4.1 Abstract data type of COCOV 32
4.2 COCOV (Compositional Concurrency Verifier) 34
4.3 The architecture 34
4.4 Grammar of abstract data type 35
4.5 Building abstract syntax tree 37
4.6 Building control flow graph 38
4.7 Model refactoring example using QUEUE 42
CHAPTER 5 DISCUSSION AND CONCLUSION 45
5.1 Discussion 45
5.2 Conclusion 46

[1] G. S. Avrunin, J. C. Corbett, M.B. Dwyer, C.S. Pasareanu, and S. F. Siegel. Comparing finite-state verification techniques for concurrent software. Technical Report UM-CS-1999-069, Dept. of CS, University of Massachusetts, November 1999. (in preaparation).
[2] K. A. Bartlett, R. A. Scantlebury, and P. T. Wilkinson. A note on reliable full-duplex transmission over half-duplex lines. Communication of ACM, 12(5):260-261, 1969.
[3] R. E. Bryant. Graph-based algorithms for Boolean function manipulations. IEEE Transactions on Computers, C-35(8):677-691, 1986.
[4] Y. Cheng. Refactoring design models for inductive verification. In Proceedings of International Symposium on Software Testing and Analysis (ISSTA2002), pages 164-168, Rome, Italy, July 2002
[5] Y.-P. Cheng, M. Young, C.-L. Hunang, and C.-Y. Pan. Towards scalable compositional analysis by refactoring design models. In Proceedings of the ACM SIGSOFT 2003 Symposium on the Foundations of Software Engineering, pages 247-256, 2003.
[6] S. C. Cheung and J. Kramer. Checking safety properities using compositional reachability analysis. ACM Transactions on Software Engineering and Methodology, 8:49-78, January 1999.
[7] J. C. Corbett. Evaluating deadlock detection methods for concurrent software. IEEE Transactions on Software Engineering, 2(3):161-180, March 1996.
[8] J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C.S. Pasareanu, Robby, and H. Zheng. Bandera: extracting finite-state models from java source code. In International Conference on Software Engineering, pages 439-448, 2000.
[9] S.Graf and B. Steffen. Compositional minimization of finite state systems. In Proceedings of the 2nd International Conference of Computer-Aided Verification, pages 186-204, 1990.
[10] K. Havelund and T. Pressburger. Model checking JAVA programs using JAVA pathfinder. International Journal on Software Tools for Technology Transfer, 2(4):366-381, 2000.
[11] D. P. Helmbold and D. C. Luckham. Debugging Ada tasking programs. In Proceedings of the IEEE Computer Society 1984 Conference on Ada Applications and Environments, pages 96-105, St. Paul, October 1984.
[12] G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, NJ 07632, 1991.
[13] G. J. Holzmann. The model checker SPIN. Software Engineering, 23(5):279-295, 1997
[14] G. J. Holzmann. Designing executable abstractions. In Proceedings of the second workshop on formal methods in software practice, pages 103-108, Clearwater Beach, Florida USA, March 1998.
[15] R. K. Keller, M. Cameron, R. N. Taylor, and D. B. Troup. User interface development and software environments: The Chiron-1 system. In Proceedings of the Thirteenth International Conference of Software Engineering, pages 208-218, Austin, TX, May 1991.
[16] K. L. McMillan. Symbolic model checking. Kluwer Academic Publishers, Massachusetts, 1993.
[17] R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1980.
[18] D. J. Richardson, S. L. Aha, and T. O. O’Malley. Specification-based test oracles for reactive systems. In Proceedings of the Fourteenth International Conference on Software Engineering, pages 105-118, Melbourne, Australia, May 1992.
[19] W. J. The and M. Young, Re-designing tasking structure of Ada programs for analysis: A case study. Software Testing, Verification, and Reliability, 4:223-253, 1994.
[20] M. Young, R. Taylor, D. Levine, K. A. Nies, and D. Brodbeck: A concurrency analysis tool suite for Ada programs: Rationale, design, and preliminary experience. ACM Transactions on Software Engineering and Methodology, 4(1):65-106, Jan 1995.
[21] A. pnueli, A temporal logic of concurrent programs, Theoretical Computer Science, vol.13, pp. 45-60, 1981.
[22] M.Y. Vardi, and Wolper, P, An automata-theoretic approach to automatic program verification, in Proc. of the 1st Symposium on Logic in Computer Science, Cambridge, June 1986, pp. 322-331, 1986
[23] K. K. Sabnani, A. M. Lapone, and M. Ű. Uyar. An algorithmic procedure for checking safety properties of protocols. IEEE Transactions on Communications, 37(9):940-948, September 1989.
[24] E. Koutsofios and S. C. North. Drawing graphs with dot AT&T Bell Labtoratories, Murray Hill, NJ.
[25] C. L. Huang Generating State Graph from Abstract Syntax Tree for Unified Refactoring Transformation to Avoid State Explosion Compositionally, Master Thesis. Dept. of Info. And Comp. Education. NTNU, 2003.
[26] C. Pan. An Extended Promela Parser Which Generates Compact CCS State Graphs Using Data Flow Analysis For Refactoring Automation. Master Thesis, Dept, Info. And Comp. Education, NTNU, 2003.