近年來，局部性分析在自動化軟體檢驗領域中佔有一席之地，是相當有前景的研究方向。局部性分析能夠成功的關鍵在於被檢驗的系統有良好的模組架構。利用合併及最小化的技術，我們可以取得子系統的介面行程。介面行程可以忽略內部行為而代表子系統，如此重覆進行局部性分析可以藉此減緩組態爆炸。
模擬是一種樂觀性的品質保證，雖然不能證明錯誤不存在，但是它的實用性在產業界和應用領域已得到很好的例證。模擬的好處之一在於其避免記錄大量的狀態而造成實體記憶體不夠的問題。只要盡可能花時間檢驗系統模型，對系統本身的正確性就更有信心。
在本篇論文中，我們將模擬和局部性分析結合在一起。利用局部性分析所取得的介面行程，只要模擬的路徑行經它，就可以視為已經拜訪過該介面行程所代表的子系統。這樣做的好處可以大大縮減模擬拜訪的深度。我們的simulator建立在既有的ArCats架構之上，運用物件導向的多型技巧，讓模擬運行在CFG（Control Flow Graph）與CCS（Calculus of Communicating System）兩種CFSM中。本篇論文會以實際的例子說明模擬結合局部性分析的好處，同時在實驗中評估其價值。

In recent years, compositional analysis in the automatic verification techniques is known as a promising approach. The states in subsystem can be minimized and hidden to alleviate state explosion while building the interface process that represents the whole subsystem. However, the key of success relies on a good modularity in system architecture. Some systems are still not amenable to compositional analysis. Simulation is an optimistic quality assurance like testing. Simulation can avoid exhausting memory while exploring state space. In the area of hardware validation, it is practical but cannot provide assurance in absence of errors. Given enough time, critical errors may still be manifested by simulation technique.
In the paper, we combine simulation and compositional analysis together. Processes in a subsystem are composed into an interface process. Simulation that walks into the interface process is equal to walk a lot of hidden states in the subsystem. The simulator of ArCats runs in the two different graph, CFG (Control Flow Graph) and CCS (Calculus of Communicating System), with polymorphism technique in OOP. The advantages of simulation with compositional analysis are shown by examples and evaluation.

[1] Holzmann, G. J. “The model checker SPIN.” IEEE Transaction on Software Engineering, Volume 23, Issue 5 : 279-295, May 1997.
[2] Holzmann, G. J. “The SPIN Model Checker: Primer and Reference Manual” Pearson Educational, 2003.
[3] Godefroid, Patrice. “Model Checking for Programming Languages using VeriSoft.” In 24th ACM Symposium onPrinciples of Programming Languages, pp. 174-186, Paris. 1997.
[4] Godefroid, Patrice. “Software Model Checking: The VeriSoft Approach.” Formal Methods in System Design 26(2): 77-101, 2005.
[5] Jurgen Dingel. “Compositional analysis of C/C++ programs with VeriSoft.” Acta informatica 43:45-71, 2006.
[6] Cheng Yung-Pin, Young, Michal, Huang, Che-Ling and Pan, Chia-Yi. “Towards Scalable Compositional Analysis by Refactoring Design Models.” ACM Software Engineering Notes, pp. 247-256, Vol 28, Issue 5, 2003.
[7] Cleaveland, R. , Parrow, J., and Steffen, B. “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.
[8] Clarke, E. M., Grumberg, O. and Peled, Doron A. “Model Checking”, MIT press, 2000.
[9] Clarke, E. M., Emerson, E.A., and Sistla, A. P. “Automatic Verification of Finite-state Concurrent Systems Using Temporal Logic Specifications,” TOPLAS, vol. 8, no.2, April, pages 244-263, 1986.

[10] Graf, S. and Steffen, B. “Compositional Minimization of Finite State Systems,” pages 186-196, CAV 1990.
[11] Yeh, W.-J. and Young, M. “Compositional Reachability Analysis Using Process Algebra,” TAV4, pages 49-59, 1991.
[12] Cheng, Yung-Pin, “Refactoring Design Models for Inductive Verification,” Proceedings of the ACM SIGSOFT 2002 Internaltional Symposium on Software Testing and Analysis. Rome, Italy, July 22-24, 2002.
[13] Michal Young, Richard N. Taylor, “Rethinking the Taxonomy of Fault Detection Techniques,” Proceedings of the 11th International Conference on Software Engineering, Pittsburgh, May 1989.
[14] S.C. Cheung, D. Giannakopoulou, J. Kramer. “Verification of Liveness Properties using Compositional Reachability Analysis,” In 5th ACM SIGSOFT Symposium on Foundations of Sofware Engineering, pages 227-243, Zurich, Switzerland, Sep, 1997.
[15] 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.
[16] 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.
[17] Hong-Yi Wang, master thesis. “On-the-fly Bisimulation Minimization in Compositional Analysis,” NTNU 2005.
[18] Amit Goel, Randal E. Bryant, “Symbolic Simulation, Model Checking and Abstarction with Partially Ordered Boolean Functional Vectors,” CAV2004, page 255-267.

[19] Bryant, R. E. “Graph-based algorithms for Boolean function manipulations.” IEEE Transactions on Computers, Vol. C-35, No. 8, pp677-691, 1986.
[20] Farn Wang, Geng-Dian Huang, Fang Yu, “Symbolic Simulation of Real-Time Concurrent Systems,” RTCSA 2003, page 595-617.
[21] Cheng, Yung-Pin, The ArCats Reference Website, Available from http://www.ice.ntnu.edu.tw/~ypc/ArCats.htm
[22] Stephan merz, “Model Checking: A Tutorial Overview,” ACM, 2001.
[23] Yu-ru Chen, master thesis, “Explicit Compositional State-Space Enumeration with Context Constraint & Counter Examples by Hierarchical Tracing.” NTNU 2005.
[24] 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, page 115-125. Los Angeles, California, Dec 1993.
[25] C.A.R Hoare. “Communicating Sequential Processes.” Prentice-Hall International, 1985.
[26] R. Milner. “Communication and Concurrency.” Prentice-Hall, Englewood Clifffs, N.J., 1989.
[27] R. Milner. “A Calculus of Communicating System.” Vol92 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1980.
[28] Godefroid, P. and Wolper, P. “A Partial Approach to Model Checking” LICS 1991, pp.406-415.
[29] Moshe Y. Yardi, “An Automata-Theoretic Approach to Linear Temporal Logic.” In F. Moller and G. Birtwistle, editors, Logics for Concurrency: Structure vs. Automata, vol 1043 of LNCS, pp. 238-266, Springer-Verlag, Berlin, 1996.
[30] E. Madelaine and R. de Simone. “The FC2Tools User Manual.” Available from ftp://ftp-sop.inria.fr/meije/verif/fc2.userman.ps, INRIA.
[31] E. Madelaine and R. de Simone. “Fc2 format Reference Manual.” Available from ftp://ftp-sop.inria.fr/meije/verif/fc2.refman.ps, INRIA.