近幾年來，自動驗證分析（automated finite-state verification）已逐漸發展成熟，但是組態爆炸（state-space explosion）的問題仍然是自動驗證分析的致命傷。許多人對於組態爆炸提出解決之道。但是由於受限於理論上的侷限，每個方法的有效與否都具有特殊性。迄今沒有一種方法使得減緩組態爆炸的成效，能夠廣泛被業界所接受。而眾多減緩組態爆炸的方法中，運用局部性分析（compositional analysis）是被公認為較具有潛力的。
局部性分析的方法就是將原有的系統分割成許多小系統，使之成階層式的架構進行分析。但是局部性分析依賴一個系統的模組性是否良好，很不幸的，大部分複雜系統並不具備這樣的模組性。因此，針對這個問題，我們提出Refactoring的方法:透過一些等價的轉換來打破系統舊有的模組性，以創造出新的系統架構，這樣新的系統架構能夠讓局部性分析發揮divide and conquer的效益。
在本研究中，我們修改SPIN的設計語言--PROMELA，除了實作PROMELA之外，並且加入了Refactoring的語法以自動化Refactoring。這個新的語法叫做rc-Promela。我們建立了rc-Promela的語法分析器, 將輸入轉換成AST樹（abstract syntax tree）。最後運用資料流分析（Data Flow Analysis）分析PROMELA程式碼，以降低展開狀態圖之狀態空間，減少組態爆炸發生的可能性。

Automated finite-state verification techniques have matured considerably in the past decades, but state-space explosion remains an obstacle to their use. Theoretical lower bounds on complexity imply that all of the techniques that have been developed to avoid or mitigate state-space explosion depend on models that are “well-formed” in some way, and will usually fail for other models. This further implies that, when analysis is applied to models derived from designs or implementations of actual software systems, a model of the system “as built” is unlikely to be suitable for automated analysis. In particular, compositional hierarchical analysis (where state-space explosion is avoided by simplifying models of subsystems at several levels of abstraction) depends on the modular structure of the model to be analyzed. We describe how as-built finite-state models can be refactored for compositional state-space analysis, applying a series of transformations to produce an equivalent model whose structure exhibits suitable modularity.
In this thesis, we adopt Promela the as front-end language to automate refactoring. We select a subset of Promela and add some keywords for refactoring. The extended syntax is called rc-Promela, where “r” stands for “refactor” and “c” stands for “ccs.” We build a parser for rc-Promela, and use the parser to construct AST for rc-Promela model. Finally, we apply data flow analysis on AST to generate compact CCS state graphs for refactoring.

References
[1]. Robin Milner, A Calculus of Communicating Systems, LNCS, vol.92, 1980.
[2]. S. C. Cheung and J. Kramer. Context constraints for compositional reachability analysis. ACM Transactions on Software Engineering and Methodology, 5(4):334-377, October 1996.
[3]. 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.
[4]. Yung-Pin Cheng and Michal Young, Semi-Automated Refactoring of Design Models for Compositional Analysis. Working Conference on Complex and Dynamic Systems Architecture, pp. 137-139 Brisbane, Australia, December, 2001.
[5]. 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
[6]. W. J. Yeh and M. Young. Compositional reachability analysis using process algebra. In Proceedings of the Symposium on Software Testing, Analysis, and Verification (TAV4), pages 49-59, Victoria, British Columbia, October 1991. ACM SIGSOFT, ACM Press.
[7]. R. M. Burstall and J. Darlington. A transformation system for developing recursive programs. JACM, 24(1):44-67, 1977.
[8]. A. Pettorossi and M. Proietti. Transformation of logic programs: Foundation and technique. Journal of Logic Programming, 1994.
[9]. 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. Edu. NTNU, 2003.
[10]. Gerard J. Holzmann. The Model Checker SPIN. IEEE Trans. Softw. Eng., 23(5):279-295, May 1997
[11]. 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 on Software Engineering, pages 208–218, Austin, TX, May 1991.
[12]. 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.
[13]. A. Pnueli, A Temporal Logic of Concurrent Programs, Theoretical Computer Science, vol. 13, pp. 45-60, 1981.
[14]. P. Wolper, An Introduction to Model Checking, in Proc. of the Software Quality Week (SQW'95), San Francisco, May, 1995.
[15]. K.L. McMillan, Symbolic Model Checking: Kluwer Academic Publishers, 1993.
[16]. G. J. Holzmann, Design and Validation of Computer Protocols: Prentice Hall,1991
[17]. G. J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering,vol. 23(5), pp. 279-295, May 1997.
[18]. G. J. Holzmann, and Peled, D, The State of SPIN, in Proc. of the 8th International Conference on Computer-Aided Verification (CAV'96), New Brunswick, NJ, USA, July/August 1996. Lecture Notes in Computer Science 1102, pp. 385-389. R. Alur and T. A. Henzinger, Eds.
[19]. 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.
[20]. 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 preparation).
[21]. 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.
[22]. J. C. Corbett. Evaluating deadlock detection methods for concurrent software. IEEE Transactions on Software Engineering, 2(3):161–180, March 1996.
[23]. 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.
[24]. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985