在軟體驗證領域中，模型檢測（Model Checking）技術是最被認可的方法之一，但最常遇到的困難，就是在建構系統模型時，常因記憶體資源不足而發生組態爆炸的問題（State Explosion Problem）。故為了提升模型檢測的可行性，有人提出局部分析（Compositional Analysis），這類技術利用原本系統的架構將一個大系統分割成許多子系統，以階層的方式來做驗證，並有效減少子系統中不必要的內部行為（internal behaviors），以避免一次整體分析可能造成的組態爆炸問題。

　　然而，局部分析還是有發生組態爆炸的可能性，如系統的階層架構不良，或是切割的子系統仍舊太大，都極可能讓局部分析失效。故在這篇論文中，我們選用Branching Bisimulation Minimization的化減技術，以得到一個組態空間較小但表現行為等價的系統模型。且Branching Bisimulation具有許多優於其他等價關係的特性，化減後仍可保留系統模型的必然性（liveness），其演算法也具有較佳的效率。然而，傳統的化減技術都是預設子系統模型已存在的情況下來執行，但大部分實際情況，在建構子系統時即已發生組態爆炸的問題。故我們提出即時化減的技術—On-the-fly Branching Bisimulation Minimization，在建構模型的過程中即先行化減的動作，讓內部行為所佔的記憶體空間，在狀態展開的過程中即可被釋放出來，以避免組態爆炸，而有效提高局部分析的可行性。

Model checking is a promising approach to analyze concurrent programs. However, enumerating the whole system model at once often leads to the problem of state explosion. In order to make it more practical, compositional analysis is presented. It verifies a system model in a hierarchical manner, and reduces unconcerned internal behaviors after each composition of subsystem.

In our thesis we choose the Branching Bisimulation Minimization [26][27] to obtain a smaller but equivalent model with regard to the original composed one. Branching Bisimulation has several nice properties better than other equivalences. It preserves liveness properties and allows more efficient algorithm to be built. Nonetheless, Branching Bisimulation Minimization is typically performed after the whole state space is enumerated completely. In the worst case, explored state space can already trigger state explosion even it can be minimized considerably. So, we propose an on-the-fly Branching Bisimulation Minimization which is integrated with our parallel composition engine. It minimizes the state space while composing to certain extent, and releases unnecessary memory space for further state enumerations. This approach alleviates the state explosion problem, therefore, increase the scalability of compositional analysis because internal behaviors in a composed subsystem can be reduced intermediately.

[1] E.M. Clarke, O. Grumberg, and Doron A. Peled. Model Checking. MIT Press, 2000.
[2] R. Cleaveland, J. Parrow, and B. Steffen. The Concurrency Workbench: A Semantics Based Tool for the Verification of Concurrent Systems. Workshop on Automatic Verification Methods for Finite State Machines, LNCS 407, pages 24-37, Feb, 1991.
[3] R. Milner. A Calculus of Communicating Systems. Vol. 92 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1980.
[4] R. Milner. Communication and Concurrency. Prentice-Hall, Englewood Cliffs, N.J., 1989.
[5] C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985.
[6] A. Pnueli. A temporal logic of concurrent programs. Theoretical Computer Science, vol.13, pp. 45-60, 1981.
[7] M.Y. Vardi and P. Wolper. 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.
[8] R.E. Bryant. Graph-based algorithms for boolean function manipulations. IEEE Transactions on Computers, Vol. C-35, No. 8, pp 677-691, 1986.
[9] J.C. Corbett. Evaluating deadlock detection methods for concurrent software. IEEE Transactions on Software Engineering, 2(3):161-180, March 1996.
[10] S.C. Cheung and J. Kramer. Checking safety properties using compositional reachability analysis. ACM Transactions on Software Engineering and Methodology, Jan, 1999, vol. 8, pp.49-78.
[11] S.C. Cheung, D. Giannakopoulou, and 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, September 1997.
[12] S. Graf and B. Steffen. Compositional Minimization of Finite State Systems. In Proc. 2nd International Conference of Computer-Aided Verification, New Brunswick, NJ, USA, June 1990, published in LNCS 531, pp. 186-196.
[13] W.J. Yeh and M. Young. Compositional Reachability Analysis Using Process Algebra. TAV4, pp 49-59, 1991.
[14] W.J. Yeh. Controlling State Explosion in Reachability Analysis. Ph.D. dissertation, SERCTR-147-P, SERC, Purdue University, December 1993.
[15] W.J. Yeh and M. Young. Redesigning Tasking Structure of Ada programs for Analysis: a Case Study. Software Testing, Verification, and Reliability, Vol. 4, pp. 223-253, 1994.
[16] S.C. Cheung and J. Kramer. Enhancing Compositional Reachability Analysis with Context Constraints. In Proc. 1st ACM International Symposium on the Foundations of Software Engineering, ACM SIGSOFT, Los Angeles, California, December 1993, pp. 115-125.
[17] S.C. Cheung and J. Kramer. Context Constraints for Compositional Reachability Analysis. ACM Transactions on Software Engineering and Methodology 5, 4 (October 1996), pp. 334-377.
[18] Y.P. Cheng and Young, M. Semi-Automated Refactoring of Design Models for Compositional Analysis. Working Conference on Complex and Dynamic Systems Architecture, pp. 137-139 Brisbane, Australia, December, 2001.
[19] Y.P. Cheng. Refactoring Design Models for Inductive Verification. Proceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis. Rome, Italy, July 22-24, 2002
[20] Y.P. Cheng, M. Young, C.L. Huang, and C.Y. Pan. Towards Scalable Compositional Analysis by Refactoring Design Models. ACM Software Engineering Notes, pp. 247-256, Vol. 28, Issue 5, 2003.
[21] Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani. Partial-Order Reduction in Symbolic State Space Exploration. CAV 1997, pp. 340-351
[22] P. Godefroid and P. Wolper. A Partial Approach to Model Checking. LICS 1991, pp. 406-415.
[23] A.P. Sistla, and K. Gyuris, and E.A. Emerson. SMC: a symmetry-based model checker for verification of safety and liveness properties. ACM Transactions on Software Engineering and Methodology, vol. 9, no. 2, pp. 133-166, 2000.
[24] 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, pp. 613-618.
[25] J.-C. Fernandez. An implementation of an efficient algorithm for bisimulation equivalence. Science of Computer Programming, 13:219-236, 1989/1990.
[26] J.F. Groote and F. Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. ICALP, 1990.
[27] A. Bouali. Weak and Branching Bisimulation in Fctool. Technical Report 1575, INRIA, Sophia Antipolis, Valbonne Cedex, France, 1992.
[28] W.J. Yeh and M. Young. Hierarchical tracing of concurrent programs. Proc. 3rd lrvine Software Symposium, pp 73-84, Costa Mesa, CA, April 1993.
[29] K. Fisler, M.Y. Vardi. Bisimulation Minimization in an Automata-Theoretic Verification Framework. FMCAD 1998: 115-132
[30] P.C. Kanellakis and S.A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. In ACM Symposium on Principles of Distributed Computing, pp 228-240, 1983.
[31] A. Aho, J. Hopcroft, and J. Ullman. Design and analysis of computer algorithms. Addison-Wesley, 1974.
[32] Thomas H. Cormen and Charles E. Leiserson. Introduction to Algorithms. MIT, 2001.
[33] Jeff Magee and Jeff Kramer. Concurrency: State Models & Java Programs. John-Wiley, 1999.
[34] Gerard J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2003.
[35] E. Madelaine and R. de Simone. The FC2 Reference Manual. Available from ftp://ftp-sop.inria.fr/meije/verif/fc2.userman.ps, INRIA.
[36] 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.