局部性分析技術對於某些系統可以有效的減緩組態爆炸，但是現有的軟體驗證工具皆少著墨於支援這部分的功能。其主要的問題在於某些系統，其架構卻不見得能組合出可分析的合成階層。其次，合成階層也難以自動化地獲得。Cheng & Young在[15]中提出一套方法稱refactoring。此方法利用CCS[12]中的weak bisimulation，將原本無法被分析的系統透過分割與轉換後，轉變為另一個行為相等的新系統。這個新系統的模組間的關係因為較為鬆散(loosely coupled)，利用誤試(trial & error)的方式可從中找出一個可分析的合成階層。這使得局部性分析的應用範圍有極大的改善。
我們配合此技術實作出局部性分析的電腦輔助驗證的工具套件。因為Java眾多的優點，如豐富的類別函式庫、記憶體的自動管理、及跨平台的特性，我們選擇以Java作為實作的語言。在這工具套件中的主要功能包含了合成階層的編輯環境(hierarchy editor)、並行合成(parallel composition)、本文限制(context constraint)[11]、分支雙模擬(branch bisimulation)[18]、安全性質的檢驗(safety property verification)[13]。這些功能當中，合成階層對於局部性分析的成敗扮演著關鍵性的作用，而且難以自動化產生。在實際的應用中，經常需要嘗試許多種階層。因此，我們在合成階層編輯環境中提供一個可以迅速地組合階層的功能。這種功能可為局部性分析的使用者帶來相當的便利。另外，局部性分析通常配合本文限制會有更大的效果。我們以Cheung & Kramer[11]中所提出的方法加以修改成以CCS語意為基礎的本文限制套件。再者，分支雙模擬套件考量其可移植性，我們重新以Java實作。最後，我們以Cheung & Kramer〔13〕中的方法，用局部性分析來檢驗安全性質，其中安全性質的檢測被轉換成一個死結偵測(deadlock detection)的問題。我們修改了該方法，使其符合CCS的語意，然後這些安全性質會被自動地加入合成階層中。經由局部性分析之後，若系統違反安全性質，則在最後的分析結果中會出現死結。

Compositional analysis can alleviate the well-known state explosion problem for some systems. However, existing computer-aided verification tools which facilitate this approach are rare. The main problem of the approach is analyzable composition hierarchy can be difficult to find in many systems. Besides, composition hierarchy is difficult to be obtained automatically. Cheng & Young in [15] overcome the problem by refactoring a system, which decomposes and transforms a system into another one with behavior equivalence preserved using weak bisimulation of CCS [12]. Refactoring often transform a system into one with loosely coupled components, which are more amenable to compositional analysis. By trial and error, we can find an analyzable composition hierarchy from the refactored architecture. It increases sociability of the compositional analysis for practical applications.

In this thesis, to aid re-factoring, we implement a compositional analysis tool suite, which adopts CCS semantics. We implement the tool suite by Java, because Java has a lot of benefits, such as rich class library, memory management automatically, and portability. The tool suite includes hierarchy editor, parallel composition, context-constraint [11], branch bisimulation [18], and safety property verification [13]. First, because the composition hierarchy often has great impact on compositional analysis, we build a hierarchy editor to allow tool users editing hierarchies easily and conveniently. Second, compositional analysis can be effective with the context-constraint. We adopt Cheung & Kramer’s approach [11], and modify it to fit CCS semantics. Third, we re-implement branch bisimulation in Java. At last, we adopt Cheung & Kramer’s approach in [13] to verify safety property with CCS semantics. Their approach translates the verification problem of safety property to a deadlock detection problem. We automatically add the safety property in the composition hierarchy. A violation of safety property will be manifested as a deadlock in the result of compositional analysis.

[1] Aho, A., J. Hopcroft, and J. Ullman. Design and analysis of computer algorithms.Addsion-Wesley, 1974.

[2] CLEAVELAND, B., A. SCOTT, SMOLKA ET AL. Strategic Directions in Concurrency Research. ACM Computing Surveys . Vol. 28. No. 4,December 1996.

[3] Bowen Alpern & F red B. Schneider. Recognizing safety and liveness. Springer-Verlag Distributed Computing(1987)2:117-126.

[4] Moshe Y. Vardi. An Automata-Theoretic Approach to Linear Temporal Logic. In Logics for Concurrency: Structures Versus Automata, Proc. of International Workshop, volume 1043 of Lecture Notes in Computer Science. Springer-Verlag, 1996.

[5] Gerard J. Holzmann The Model Checker Spin. IEEE TRANSACTION ON SOFTWARE ENGINEERING VOL 23. NO 5 MAY 1997.

[6] Gerard J. Holzmann & Anuj Puri. A Minimizing Automata Representation of Reachable States. Springer-Verlag 1999.Software Tools for Technology Transfer.

[7] R. Gerth, D. Peled, M. Y. Vardi and P. Wolper. Simple On-the-fly Automatic Verification of Linear Temporal Logic.Proc. IFIP/WG6.1 Symp. Protocol Specification, Testing , and verification(PSTV95),pp.3-18, Warsaw, Poland, Chapman & Hall, June 1995.

[8] Patrice Godefroid & Pierre Wolper. Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Property. Formal Methods in System Design, 2(2):149--164, 1993.
[9] Wei Jen Yeh & Michal Young. Compositional Reach-Ability Analysis of Ada Program Using Process Algebra. In proceedings of the symposium on testing, Analysis, and Verification (TAV4), Pages 178-187, New York, Oct, 1991. ACM SIGSOFT, Association for Computer Machinery.
[10] D. Vergamini. Auto/Mauto user manual V2-3. Technical Report (to appear),INRIA, 1991.
[11] Shing Chi Cheung & Jeff Krammer. Context Constraint for Compositional Reachability Analysis. ACM Transactions on Software Engineering and Methodology, Vol. 5, No. 4, October 1996, Pages 334-377.
[12] Robin. Milner. 1989. Communication and Concurrency. P:rentice-Hall, Englewood Cliffs, N.J.
[13] Shing Chi Cheung & Jeff Kramer. Checking Safety properties Using Compositional Reach-ability Analysis. ACM Transactions on Software Engineering and Methodology, Vol. 8, No. 1, January 1999, Pages 49-78
[14] Shing Chi Cheung, Dimitra Giannakopoulou, and Jeff Kramer. Verification of Liveness Properties Using Compositional Reach-ability Analysis.Technical Report HKUST-CS96-36,October 1996.
[15] Yung-Pin Cheng & Michal Young. Towards Scala Compositional Analysis by Refactoring Design Models. submit by journal.
[16] Amar Bouali. Weak and Branching Bisimulation in FCTOOL Equivalence Observationnlle et Branching Bsimulation dans FCTOOL. INRIA, Jan, 1992.
[17] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions Programming Language and Systems, Vol. 8, No. 2, April 1986, Pages 244-263.
[18] Jan Friso Groote,Frits Vaandrager. An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence.ICALP ’90,1990
[19] George S. Avrunin, James C. Corbett, Matthew B. Dwyer, Corina S. Pasareanu, Stephen F. Siegel. Comparing Finite-State Verification Techniques for Concurrent Software. UM-CS-1999-069, November 1999
[20] E. M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. Model Checking, The MIT press Cambridge, Massachusetts, London, England. 1999.
[21] Jamieson M. Cobleigh, Lori A. Clarke, and Leon J. Osterweil. FLAVERS：a Finite State Verification Technique for Software System. Software Testing and Verification, Volume 41, Number 1, 2002.
[22] L. K. Dillon, G. Kutty, L. E. Moser, P. M. Melliar-Smith, and Y. S. Ramakrishna.A graphical Interval Logic for Specifying Concurrent Systems. ACM Trams. On Software Engineering and Methodology, Vol 3, No 2, April 1994, pp 131-165
[23] Mattew B. Dwyer, George S. Avrunin, James C. Corbett. Property Specification Patterns for Finite-State Verification. In Proceedings of the 21st International Conference on Sfotware Engineering, pages 16-22, May 1999.
[24] Rance Cleaveland, Joachim Parrow, Bernhard Steffen.The Concurrency Workbench：A Semantics-Based Tool for the Verification of Concurrency Systems. ACM Trans. Prog. Lang. Syst. 15(1):36-72, Jan. 1993.
[25] Claudc Jard. Thicrry Jc’ron Jcan-Claudc Fcrnandcz. On-the-fly Verification of Finite Transition Systems. In Computer-Aided Verification, R. Kurshan, Ed. ; Kluwer Academic Publishers, 1993.
[26] C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall International, 1985.