使用重構技術和設計模式進行ARCATS既有架構的改良
No Thumbnail Available
Date
2010
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
局部性分析（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.
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.
Description
Keywords
模型驗證, 局部性分析, ARCATS, 狀態空間展開, 重構, Model Checking, Compositional Analysis, ARCATS, State Space Enumeration, Refactoring