2 未來展望

在本篇論文中，我們將 ArCats 局部性分析工具，重構為一具有演化性和擴 充性的物件導向架構系統，最終的用意就是希望在往後增加合成規則和進行不同

LTS 模型分析時，程式的撰寫能夠不僅容易擴充，並大幅降低維護和 debug 的成 本，加速系統開發的速度。

目前 ArCats 是以 CCS 的 LTS 為主要分析模型，未來我們希望加入 CSP -based 的 LTS 模型，使得 ArCats 局部性分析工具所分析的模型可以更多元化。另外我 們也預計加入其它合 成規則於重構後的局部性分析工具中，例如 Liveness

Property 的檢驗。

此外，我們也希望藉由這樣富有彈性的架構，可以藉由各個合成規則間的組 合，提供未來理論研究時的實作，例如在檢驗安全性質時，是否可以一併進行本 文限制的化減，或是使用即時化減技術進行狀態的最小化，以真正發揮局部性分 析的優點。

在合成引擎未來的改進方向中，我們也可以針對每個狀態的資料結構儲存方 式加以改良，例如使用資料壓縮技術。在狀態展開使用各種技術予以簡化的同 時，也可以從狀態佔有記憶體的空間著手，試圖達到最小化或是更為精簡，以降 低局部性分析面臨組態爆炸此最大難題的可能。

Reference

[1] Bryant, R. E. Graph-based algorithms for Boolean function manipulations. IEEE Transactions on Computers, Vol. C-35, No. 8, pp677-691, 1986.

[2] Clarke, E. M., Grumberg, O. and Peled, Doron A. Model Checking, MIT press, 2000.

[3] C.A.R Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985.

[4] D.J. Richardson, S.L. Aha, and T.O. O’Malley. Specification-based test oracles for reactive system. In Proceedings of the Fourteenth International Conference on Software Engineering, pages 105-118, Melbourne, Australia, May 1992.

[5] E. Madelaine and R. de Simone. The FC2Tools User Manual, http://www-sop.inria.fr/meije/verification/, 1999, INRIA.

[6] E. Madelaine and R. de Simone. Fc2 format Reference Manual, http://www-sop.inria.fr/meije/verification/, 1999, INRIA.

[7] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent system using temporal logic. ACM Transactions on Programming Languages and Systems,8（2）:244-263,April 1986.

[8] E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns: Elements of Reusable Object-oriented Software. Addison-Wesley, Reading, Mass. 1995.

[9] G. J. Holzmann, The model checker SPIN. IEEE Transaction on Software Engineering, Volume 23 , Issue 5 : 279-295,May 1997 .

[10] G. R. Andrews, Concurrent Programming – Principles and Practice. The Benjamin/Cummings Publishing Company Ltd., 1991.

[11] Gian-Luigi Ferrari, Stefania Gnesi, Isti-C.N.R.Pisa, Marco Pistore. A

[12] Graf, S. and Steffen, B. Compositional Minimization of Finite State Systems, pages 186-196, CAV 1990.

[13] Godefroid, P. and Wolper, P. A Partial Approach to Model Checking. LICS 1991, pp.406-415.

[14] G. G. Koni-N’Sapu. Supremo, A scenario based approach for refactoring duplicated code in object oriented systems. Diploma thesis, University of Bern, June 2001.

[15] Holzmann, G. J. The model checker SPIN. IEEE Transaction on Software Engineering, Volume 23, Issue 5 : 279-295, May 1997.

[16] Holzmann, G. J. State Compression in SPIN: Recursive Indexing and Compression Training Runs, In Proceedings of Third International SPIN Workshop .1997.

[17] Holzmann, G. J. The SPIN Model Checker: Primer and Reference Manual.

Pearson Educational, 2003.

[18] Hong-Yi Wang master thesis. On-the-fly Bisimulation Minimization in Compositional Analysis. NTNU 2005.

[19] Kim, M., Bergman, L, Lau, T., and Notkin, D. An Ethnographic Stud of Copy and Paste Programming Practices in OOPL. International Symposium on Empirical Software Engineering, 2004.

[20] Larsen. K. and Milner, R. Verifying a protocol using relativized bisimulation.

In proceedings of the 14^th International Colloquium on Automata language and Programming. 1987.

[21] L. Tokuda and D.S. Batory, Evolving Object-Oriented Designs with Refactorings, Automated Software Engineering, 8, 89–120, 2001

[22] Malhotra J. Smolka, S. A. Giacalone and Shapir R. A tool for hierarchical design and simulation of concurrent systems. In Proceedings of the BCS-FACS Workshop on Specification and Verification of Concurrent Systems, 1988.

[23] Martin. Fowler. Refactoring: Improving The Design Of Existing Code.

Addison-Wesley, 1999.

[24] R. Milner. Communication and Concurrency. Prentice-Hall, Englewood Clifffs, N.J., 1989.

[25] R. Milner. A Calculus of Communicating System. Vol92 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1980.

[26] R.J. Van Glabbeek and W. Peter Weijland, Branching Time and Abstraction in Bisimulation Semantics (extended abstract). In information Processing 89, G.

Ritter, ed., North-Holland, 1989, pages 613-618.

[27] S.C. Cheung, D. Giannakopoulou, J. Kramer. Verification of Liveness Properties using Compositional Reachability Analysis, In 5th ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 227-243, Zurich, Switzerland, Sep, 1997.

[28] S.C. Cheung and J. Kramer. Checking Safety Properties using Compositional Reachability Analysis, ACM Transactions on Software Engineering and Methodology, Jan, 1999, vol. 8, page 49-78.

[29] Shing Chi Cheung and Jeff Kramer. Context Constraints for Compositional Reachability Analysis. ACM 1996.

[30] T. Mens and T. Tourw´e. A survey of software refactoring. IEEETransactions on Software Engineering, 30(2):126–139, Feb. 2004.

[31] Yeh, W.-J. and Young, M. Compositional Reachability Analysis Using Process Algebra, TAV4, pages 49-59, 1991.

[32] Yung-Pin Cheng. The ArCats reference.

U

http://www.csie.ntnu.edu.tw/~ypc/ArCats.htm

[33] Yu-ju Cheng master thesis. Explicit Compositional State-Space Enumeration with Context Constraint & Counter Examples by Hierarchical Tracing. NTNU 2005.

[34] Zhi-Wen Hsu master thesis. Compositional Model Checking Safety and Liveness Properties in ARCATS. NTNU 2006.