簡易檢索 / 詳目顯示

回結果列表
研究生： 傅心儀
論文名稱： 使用重構技術和設計模式進行ARCATS既有架構的改良
Refactoring ARCATS for Maintainability and Evolvability by Design Patterns
指導教授： 鄭永斌
學位類別： 碩士
Master
系所名稱： 資訊工程學系
Department of Computer Science and Information Engineering
論文出版年： 2010
畢業學年度： 98
語文別： 中文
論文頁數： 64
中文關鍵詞： 模型驗證 、局部性分析 、ARCATS 、狀態空間展開 、重構
英文關鍵詞： Model Checking, Compositional Analysis, ARCATS, State Space Enumeration, Refactoring
論文種類： 學術論文
相關次數： 點閱：183  下載：1 
分享至:
查詢本校圖書館目錄 查詢臺灣博碩士論文知識加值系統 勘誤回報

    • 局部性分析（Compositional Analysis）在軟體模型驗證(Model Checking)領域中被認為是該技術邁入實用化的重要關鍵技術。局部性分析之所以能夠成功，關鍵在於被檢驗的模型系統具備良好的模組架構，以階層式逐步分析並合成各個子系統，以達到分析整個系統的目的。在合成子系統的過程中並採用各種簡化技術以達到狀態空間的最小化，減緩組態爆炸的發生。
    ArCats（Architecture Refactoring Compositional Analysis Tool Suite）即是依據此理論基礎所發展的局部性分析軟體驗證工具。ArCats的合成引擎（Composition Tool）在列舉展開一個代表子系統行為的狀態空間（State Space）的過程中，以本文限制（Context Constraint）與簡化子系統（Reduction or Minimization）來降低組態爆炸（State Explosion）的問題，並在合成時一併檢測系統安全性質（Safety Property）。
    在上述所提到的功能中，由於彼此間有著頻繁的合作且功能重複的特性，故以往的實作時皆copy-paste原有的程式碼再予以修改，以因應新功能的加入，造成系統維護和修改成本大幅提高。由於合成狀態的功能在模型驗證技術上具有核心的關鍵位置，在軟體開發的過程中，此類工具的程式碼若缺乏架構，導致無法重用與兼容，將會是後續專案開發上的阻力。隨著研究的進展，列舉狀態空間時所使用的合成規則，以及模型驗證工具欲檢驗性質的增加，缺乏彈性的實作方式僅會加深程式碼的晦澀，專案難以維護以及功能難以擴充。
    本研究欲提出一個方法，將欲檢驗的性質和合成規則集中，在局部性分析列舉狀態時可隨時組合或是單獨使用這些合成規則。往後若需要分析不同型態的系統模型，亦可以輕易運用既有的合成規則，使得程式碼重覆利用，減輕專案開發的負擔。不僅可以讓程式碼更具彈性和擴充性，並期盼可以提供了更多規則的組合方式，以提供後續更深入的理論研究。

    Compositional Analysis is considered as a promising approach for scalability in the field of model checking. The success of composition analysis, however, depends on a good modularity in system architecture to verify a system in a hierarchical manner. In the hierarchical composition, there are several reduction and minimization techniques which can be applied to mitigate its state space efficiently.

    ArCats (Architecture Refactoring Compositional Analysis Tool Suite) is a model checking tool which support compositional analysis. The composition tool of ArCats is capable of composing reachable state space with context constraint, on-the-fly minimization by branch bisimulation and safety property verification.

    Previous implementations often use copy-paste programming to accomplish their tasks. The cost of maintenance and debugging is high when the system needs to be changed. Because the enumeration of states is a core feature that involves a lot of composition rules, it is unfortunately tangled by a lot of functionality and creates a lot of maintenance problems.

    We propose an approach to refactor the whole system by centralizing the composition rules in a Rule Engine. While exploring state space the new system allows different combinations of rules, all based on a program. Our approach also keeps code readable and maintainable by refactoring. Eventually, we bring maintainability and evolvability to ArCats.

    摘要 2 Abstract 3 圖表目錄 6 表格目錄 7 Chapter 1 緒論 8 Section 1.1 研究動機 8 Section 1.2 論文架構 13 Chapter 2 研究背景 15 Section 2.1 Labeled Transition System（LTS） 15 Section 2.2 平行合成（Parallel Composition） 17 2.2.1. Two-Way Rendezvous 18 2.2.2. Multi-Way Rendezvous 19 Section 2.3 狀態空間的展開（State Space Enumeration） 20 2.3.1. Reduction：狀態空間的化減 20 2.3.2. Minimization：狀態空間的最小化 21 Section 2.4 局部性分析（Compositional Analysis） 22 Section 2.5 ArCats與其它模型驗證工具 23 2.5.1. SPIN 23 2.5.2. FC2Tools 23 2.5.3. ArCats 24 Chapter 3 ArCats合成規則分析與即時化減技術 25 Section 3.1 基本合成規則 26 Section 3.2 本文限制（Context Constraint） 27 3.2.1. 環境介面行程(Environment Interface Process) 27 3.2.2. 本文限制的合成規則 29 Section 3.3 安全性質（Safety Property） 32 3.3.1. 安全性質的合成規則 33 Section 3.4 即時化減技術 37 Chapter 4 重構ArCats局部性分析工具 39 Section 4.1 重構前的合成引擎架構 39 Section 4.2 重構後的合成引擎架構 42 4.2.1. 消除重複的程式碼：合成引擎的改良 43 4.2.2. 多型取代條件式：合成規則引擎實作和最小化引擎的改良 45 Section 4.3 重構後的架構圖 50 Chapter 5 評估 52 Section 5.1 減少不必要的程式碼 52 Section 5.2 彈性和擴充性 53 5.2.1. 合成規則的組合與加入即時化減技術 53 5.2.2. 新增LTS型態 55 Section 5.3 程式執行效能 57 Chapter 6 結論與未來展望 59 Section 6.1 結論 59 Section 6.2 未來展望 60 Reference 61

    [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 model-checking Verification Environment for Mobile Processes. ACM 2003.
    [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 14th 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. IEEE Transactions 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. http://www.csie.ntnu.edu.tw/~ypc/ArCats.htm, 2007
    [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.

    下載圖示
    QR CODE