並行機制(concurrency)的引進提供給軟體系統更多的效能，不幸的是，這使的原本就不易檢驗的系統正確性變的更加困難。通常關鍵性系統(critical systems)可能因為發生系統錯誤而造成無法承受的損失，故檢驗軟體的正確性對這一類系統是相當重要的。而在現行的驗證技術中，以模型驗證(model checking)為最常見。
這類技術多半是仰賴使用者先行將待檢驗的系統，依模型檢測工具制定的模型描述語言(modeling language)輸入後才能進行正式的驗證程序。這之間的轉換過程除了會造成錯誤，也會造成許多資訊的遺失，而這也解釋了為何主要的 model checking技術離實用還有很大的距離。
直接驗證高階語言直覺上會是最自然的選擇，不過直接以程式語言進行驗證的代價並不便宜，而且有許多待突破的技術困難，例如，每一種程式語言都有其獨特的特性，而且所支援的同步與通訊指令都不相同。因此本篇論文提出了一個彈性架構，在這個架構中，我們先將未來所選定的高階語言轉換成本論文所描述的control flow graph(CFG)，目的在應付未來支援多語言輸入的支援。其目的是保留原始程式碼的資訊，讓後端模擬引擎可依 control flow graph 進行分析。此CFG 的制訂可以令後端的分析與模擬引擎，與前端語言的語法以及語意做到區隔，使模擬引擎可以支援多種程式語言的輸入。我們的目標是希望使用者在未來直接可以使用一般的程式語言建立模型，並且可以在程式開發階段就能進行初步的分析檢驗。
ArCats中的局部性分析模組，是使用CCS(Calculus of Communicating System)做為模型輸入。因此為了使修改後的 CFG 也能正確的轉換出 CCS，我們也重新實做了這個轉換的程式，並且解決新衍生的問題。

Multi-threading and multi-core technology introduce more computing power to software system, but unfortunately, concurrency makes system correctness more difficult to verify. To many critical systems, failures could cost lives and large amount of money, so the correctness plays a vital role in the development of such systems. In recent years, model checking is the most popular approach to address the problem. Model checking often requires users to abstract a model from a target system. But the abstraction process between source code and model often drives programmers away from such technique. This explains why verification tools are still far from practical usage.
Having users write model with high-level programming language is the most straightforward idea to ease the use of verification tools. Nevertheless, the cost of building and maintaining a programming language parser and its related components is high. In this thesis, we propose an intermediate data structure based on control flow graph. In the future, we expect the input program will be translated into such control flow graph. The control flow graph serves as the standard representation for our backend analysis engine.
ArCats (Architecture Refactoring and Concurrency Analysis Tool Suite) is a research prototype this work is built from. It runs in the two different graph-like data structure, CFG (Control Flow Graph) and CCS (Calculus of Communicating System), by polymorphism technique in OOP. In the compositional analysis module, we use CCS as model input. In this thesis, the component that translates the revised CFG to CCS is also described.

[1] Silberchatz, Operating System Principles, 7 ed.: John Wiley & Sons, 2004.
[2] E. M. Clarke, et al., "Automatic verification of finite-state concurrent systems using temporal logic specifications," ACM Trans. Program. Lang. Syst., vol. 8, pp. 244-263, 1986.
[3] G. J. Holzmann, "The Model Checker SPIN," IEEE Transactions on Software Engineering, vol. 23, pp. 279-295, 1997.
[4] S. Merz, "Model checking: a tutorial overview," in Modeling and verification of parallel processes, ed: Springer-Verlag New York, Inc., 2001, pp. 3-38.
[5] E. M. Clarke and B.-H. Schlingloff, "Model checking," in Handbook of automated reasoning, ed: Elsevier Science Publishers B. V., 2001, pp. 1635-1790.
[6] R. Jhala and R. Majumdar, "Software model checking," ACM Comput. Surv., vol. 41, pp. 1-54, 2009.
[7] A. Miller, et al., "Symmetry in temporal logic model checking," ACM Comput. Surv., vol. 38, p. 8, 2006.
[8] I. a. E. d. Mines/CMA. Auto/Graph and Fc2tools documentation Available:
http://www-sop.inria.fr/meije/verification/doc.html
[9] B. Boigelot and P. Godefroid, "Model Checking in Practice: An Analysis of the ACCESS.bus Protocol using SPIN," presented at the Proceedings of the Third International Symposium of Formal Methods Europe on
Industrial Benefit and Advances in Formal Methods, 1996.
[10] B. Labs. (1991, ON-THE-FLY, LTL MODEL CHECKING with SPIN Available: http://spinroot.com/
[11] J. R. Burch, et al., "Symbolic model checking:
10<supscrpt>20</supscrpt> states and beyond," Inf. Comput., vol. 98, pp. 142-170, 1992.
[12] M. Y. Vardi, "Linear-time model checking: automata theory in practice," presented at the Proceedings of the 12th international conference on Implementation and application of automata, Prague, Czech Republic,2007.
[13] P. Godefroid, "Invited Talk: "Model checking" software with VeriSoft," presented at the Proceedings of the 5th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering,Washington DC, USA, 2004.
[14] P. Godefroid, "Model checking for programming languages using VeriSoft," presented at the Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages,Paris, France, 1997.
[15] J. Dingel, "Computer-assisted assume/guarantee reasoning with VeriSoft," presented at the Proceedings of the 25th International Conference on Software Engineering, Portland, Oregon, 2003.
[16] R. Alur and R. Grosu, "Modular refinement of hierarchic reactive machines," ACM Trans. Program. Lang. Syst., vol. 26, pp. 339-369, 2004.
[17] C. Blundell, et al., "Assume-guarantee testing," presented at the Proceedings of the 2005 conference on Specification and verification of component-based systems, Lisbon, Portugal, 2005.
[18] J. Dingel, "Compositional Analysis of C/C++ Programs with VeriSoft," Acta Inf., vol. 43, pp. 45-71, 2006.
[19] J. M. J. Kramer, Concurrency: State Models & Java Programs 1999.
[20] J. K. Jeff Magee, Robert Chatley, Sebastian Uchitel, Howard Foster. LTSA - Labelled Transition System Analyser. Available: http://www.doc.ic.ac.uk/ltsa/
[21] A. P. Sistla and E. M. Clarke, "The complexity of propositional linear temporal logics," J. ACM, vol. 32, pp. 733-749, 1985.
[22] M. Musuvathi, "Systematic concurrency testing using CHESS," presented at the Proceedings of the 6th workshop on Parallel and distributed systems: testing, analysis, and debugging, Seattle, Washington,2008.
[23] E. M. Clarke, et al., "Verification Tools for Finite-State Concurrent Systems," presented at the A Decade of Concurrency, Reflections and Perspectives, REX School/Symposium, 1994.
[24] R. E. Bryant, "Symbolic Boolean manipulation with ordered binary-decision diagrams," ACM Comput. Surv., vol. 24, pp. 293-318, 1992.
[25] R. Milner, A Calculus of Communicating Systems: Springer-Verlag New York, Inc., 1982.
[26] R. Milner, Communication and concurrency: Prentice-Hall, Inc., 1989.
[27] Y.-P. Cheng. (2005, Architecture Refactoring and Compositional Analysis Tool Suite. Available: http://www.csie.ntnu.edu.tw/~ypc/ArCats.htm
[28] D. G. Fritz and R. G. Sargent, "An overview of hierarchical control flow graph models," presented at the Proceedings of the 27th conference on Winter simulation, Arlington, Virginia, United States, 1995.
[29] A. T. R. Labs. Graphviz - Graph Visualization Software. Available: http://www.graphviz.org/ [30] C. Y. Li, "Simulation with Compositional Analysis," Electronic Theses and Dissertations System, 2007.
[31] T. P. a. others, "ANother Tool for Language Recognition (ANTLR) ", 3 ed, 2007.
[32] R. C. Martin, Agile Software Development: Principles, Patterns, and Practices: Prentice Hall PTR, 2003.
[33] Wikipedia. (8 June 2010, Template method pattern. Available: http://en.wikipedia.org/wiki/Template_method_pattern
[34] Y.-P. Cheng, et al., "Towards scalable compositional analysis by refactoring design models," presented at the Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software
engineering, Helsinki, Finland, 2003.