簡易檢索 / 詳目顯示

回結果列表
研究生： 黃哲菱
論文名稱： 為了避免局部性的組態爆炸而從抽象語法樹產生狀態機繼而做統一的轉換
Generating State Graphs from Abstract Syntax Tree for Unified Transformations to Avoid State Explosion Compositionally
指導教授： 鄭永斌
學位類別： 碩士
Master
系所名稱： 資訊教育研究所
Graduate Institute of Information and Computer Education
論文出版年： 2003
畢業學年度： 91
語文別： 中文
論文頁數： 88
中文關鍵詞： refactoring 、局部性分析 、Promela 、CCS
英文關鍵詞： refactoring, compositional analysis, Promela, CCS
論文種類： 學術論文
相關次數： 點閱：218  下載：2 
分享至:
查詢本校圖書館目錄 查詢臺灣博碩士論文知識加值系統 勘誤回報

    • 近年來，有許多用來分析並行式系統(concurrent system)的技術被提出。其中，以有限狀態機(finite state machine)來做系統驗證的技術最受歡迎，因為這項技術較具實用性，且也較容易自動化。然而，這項技術在實際應用上卻會遭遇到組態爆炸(state explosion)的問題。為了解決這個問題，許多改良的技術被提出。局部性分析(compositional analysis)即為其中之一。局部性分析法是將原本的系統分割成許多小系統，再利用divide and conquer的原理進行分析，如此一來，就能夠分析較大的系統。
    然而在實際應用上，這樣的方法不一定能夠成功，因為系統本身不一定具備有良好的系統架構。所謂良好的系統架構，是指組成系統內的子系統彼此之間的關聯是較為鬆散的，如此一來，當局部分析法應用在此系統上時，較能發揮其作用。[6]提出一套refactoring的方法來解決這個問題。Refactoring是半自動化地透過一些等價的轉換來打破系統舊有的模組性以創造出新的系統架構。使得局部分析可分析的系統大小突破以往的限制。
    在本篇論文，我們實作了一個系統來達到自動化refactoring。我們將rc-Promela[17]轉換成有現狀態機。當refactoring被啟動之後，我們將每個程序轉換成許多的片段(segments)。接著，我們設計與實作unified transformations將片段包裝成新的程序。在轉換的過程中，我們必須確保行為的一致性。最後產生的新的系統架構，將使得局部分析可分析的系統大小突破以往的限制。

    In the recent years, many techniques for analyzing concurrent systems have been proposed. Among them, finite-state verification technique is attractive because it is simple and relatively straightforward to automate. However, its performance is limited by the well-known state explosion problem. Many techniques have been proposed to address the problem. Among which, compositional analysis which divides a full system into subsystems and analyzes the system in a divide and conquer manner is more promising for large-scale concurrent systems.
    In practice, compositional techniques are inapplicable to many systems because their as-built structures may not be suitable for compositional analysis. A structure suitable for compositional analysis must contain loosely coupled components so that every component can be replaced by a simple interface process. However, an ideal structure like that seldom exists in practice.
    In [6], Cheng proposed an ad hoc approach, called refactoring, to translate as-built architectures to improve compositional analysis. However, the transformations described are performed manually by ad hoc basis.
    In this thesis, we implement a system to automate the refactoring. We translate rc-Promela [17], a design language, into finite state graphs in CCS semantics [4]. If refactoring is enabled, the behaviors of processes will be translated into some smaller units, called segments. Next, we derive and implement unified transformations transform the segments into new processes. In the transformations, the behaviors of the whole system remain equivalent. As a result, the new structure allows compositional analysis to exploit new composition hierarchy to avoid state explosion.

    List of figures viii Chapter 1. Introduction 1-1 1.1 Objective 1-1 1.2 System Architecture and compositional analysis 1-2 1.3 Organization of this thesis 1-6 Chapter 2. Background 2-1 2.1 Model checking 2-1 2.2 Model checking tools 2-2 2.2.1 FC2TOOLS 2-2 2.2.2 SMV 2-3 2.2.3 SPIN 2-3 2.3 Communicating finite state machine (CFSM) 2-3 2.4 Parallel composition 2-5 2.5 Methods of state space enumeration 2-8 2.6 Compositional analysis 2-8 2.7 Related work 2-9 Chapter 3. An Overview of Refactoring 3-1 Chapter 4. Using AST to Generate CCS State Graphs 4-1 4.1 Generating communicating finite state machine 4-2 4.1.1 The general idea 4-2 4.1.2 A simple example 4-5 4.1.3 Traversing with compact product 4-7 4.1.4 Algorithm of generating CFSM 4-9 4.2 Generating segments within REFECTORBY{ } 4-12 4.2.1 How to generate segments 4-13 4.2.2 A simple example 4-15 4.2.3 Algorithm of generating segments 4-16 4.3 Communicating finite state machine (CFSM) 4-18 4.4 Parallel composition 4-21 Chapter 5. The Unified Refactoring Transformation 5-1 5.1 TransformationⅠ for guards prefixed with “ch?” 5-2 5.1.1 Value process 5-2 5.1.2 Constructing value processes 5-3 5.1.3 How to decompose state graph 5-5 5.1.4 Algorithm 5-6 5.1.5 Identify control variables 5-8 5.2 Transformation Ⅱ for guards prefixed with “” 5-9 5.3 Transformation Ⅲ for guards prefixed with “ch !” 5-11 5.4 Transformation Ⅳ for simplification 5-14 5.4.1 How to simplify state graphs 5-15 5.4.2 The Algorithm of simplification transformation 5-16 Chapter 6. Experiment Results 6-1 6.1 Tool support for compositional analysis 6-1 6.2 Examples 6-2 6.2.1 The elevator system 6-2 6.2.2 Chiron User Interface System 6-4 Chapter 7. Conclusions 7-1 References 8-1

    [1] W. J. Yeh and M. Young. Compositional reachability analysis using process algebra. In Proceedings of the ACM SIGSOFT Symposium on Testing, Analysis, and Verification (TAV4), page49–59, Victoria, British Columbia, October 1991. ACM SIGSOFT, ACM Press.
    [2] G. J. Holzmann. The Model Checker SPIN. In IEEE Transactions on Software Engineering, 23(5):279-295, May 1997.
    [3] G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, NJ 07632, 1991.
    [4] R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1980.
    [5] S. Graf and B. Steffen. Compositional minimization of finite state systems. In Proceedings of the 2nd International Conference of Computer-Aided Verification, pages 186–204, 1990.
    [6] Y. Cheng. Refactoring design models for inductive verification. In Proceedings of International Symposium on Software Testing and Analysis (ISSTA2002), pages 164–168, Rome, Italy, July 2002.
    [7] G. S. Avrunin, J. C. Corbett, M. B. Dwyer, C. S. Pasareanu, and S. F. Siegel. Comparing finite-state verification techniques for concurrent software. Technical Report UM-CS-1999-069, Dept. of CS, University of Massachusetts, November 1999. (in preparation).
    [8] M. Young, R. Taylor, D. Levine, K. A. Nies, and D. Brodbeck. A concurrency analysis tool suite for Ada programs: Rationale, design, and preliminary experience. ACM Transactions on Software Engineering and Methodology, 4(1):65–106, Jan 1995.
    [9] J. C. Corbett and G. S. Avrunin. Towards scalable compositional analysis. In Proceedings of the Second ACM SIGSOFT Symposium on Foundations of Software Engineering., pages 53–61, New Orleans, Louisiana, USA, December 1994.
    [10] W. J. Yeh and M. Young. Re-designing tasking structure of Ada programs for analysis:A case study. Software Testing, Verification, and Reliability, 4:223–253, 1994.
    [11] E. Madelaine and R. de Simone. The FC2 Reference Manual. Available by ftp from cma.cma.fr:pub/verif as file fc2refman.ps, INRIA.
    [12] D. J. Richardson, S. L. Aha, and T. O. O’Malley. Specification-based test oracles for reactive systems. In Proceedings of the Fourteenth International Conference on Software Engineering, pages 105–118, Melbourne, Australia, May 1992.
    [13] J. C. Corbett. Evaluating deadlock detection methods for concurrent software. IEEE Transactions on Software Engineering, 2(3):161–180, March 1996.
    [14] S. C. Cheung and J. Kramer. Context constraints for compositional reachability analysis. ACM Transactions on Software Engineering and Methodology, 5(4):334–377, October 1996.
    [15] S. C. Cheung and J. Kramer. Checking safety properties using compositional reachability analysis. ACM Transactionson Software Engineering and Methodology, 8:49–78, January 1999.
    [16] R. K. Keller, M. Cameron, R. N. Taylor, and D. B. Troup. User interface development and software environments: The Chiron-1 system. In Proceedings of the Thirteenth International Conference on Software Engineering, pages 208–218, Austin, TX, May 1991.
    [17] C. Pan. An Extended Promela Parser Which Generates Compact CCS State Graphs Using Data Flow Analysis For Refactoring Automation. Master Thesis, Dept, Info. and Comp. Education, NTNU, 2003.
    [18] 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.
    [19] K. K. Sabnani, A. M. Lapone, and M. Ü. Uyar. An algorithmic procedure for checking safety properties of protocols. IEEE Transactions on Communications, 37(9):940–948, September 1989.
    [20] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
    [21] A. Pnueli. A Temporal Logic of Concurrent Programs. Theoretical Computer Science, (13):45-60, 1981.
    [22] M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the first Symposium on Logic in Computer Science, pages 322-331, Cambridge, June 1986.

    QR CODE