一個PROMELA語法分析器並且運用資料流分析以產生簡潔的狀態圖
No Thumbnail Available
Date
2003
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
近幾年來,自動驗證分析(automated finite-state verification)已逐漸發展成熟,但是組態爆炸(state-space explosion)的問題仍然是自動驗證分析的致命傷。許多人對於組態爆炸提出解決之道。但是由於受限於理論上的侷限,每個方法的有效與否都具有特殊性。迄今沒有一種方法使得減緩組態爆炸的成效,能夠廣泛被業界所接受。而眾多減緩組態爆炸的方法中,運用局部性分析(compositional analysis)是被公認為較具有潛力的。
局部性分析的方法就是將原有的系統分割成許多小系統,使之成階層式的架構進行分析。但是局部性分析依賴一個系統的模組性是否良好,很不幸的,大部分複雜系統並不具備這樣的模組性。因此,針對這個問題,我們提出Refactoring的方法:透過一些等價的轉換來打破系統舊有的模組性,以創造出新的系統架構,這樣新的系統架構能夠讓局部性分析發揮divide and conquer的效益。
在本研究中,我們修改SPIN的設計語言--PROMELA,除了實作PROMELA之外,並且加入了Refactoring的語法以自動化Refactoring。這個新的語法叫做rc-Promela。我們建立了rc-Promela的語法分析器, 將輸入轉換成AST樹(abstract syntax tree)。最後運用資料流分析(Data Flow Analysis)分析PROMELA程式碼,以降低展開狀態圖之狀態空間,減少組態爆炸發生的可能性。
Automated finite-state verification techniques have matured considerably in the past decades, but state-space explosion remains an obstacle to their use. Theoretical lower bounds on complexity imply that all of the techniques that have been developed to avoid or mitigate state-space explosion depend on models that are “well-formed” in some way, and will usually fail for other models. This further implies that, when analysis is applied to models derived from designs or implementations of actual software systems, a model of the system “as built” is unlikely to be suitable for automated analysis. In particular, compositional hierarchical analysis (where state-space explosion is avoided by simplifying models of subsystems at several levels of abstraction) depends on the modular structure of the model to be analyzed. We describe how as-built finite-state models can be refactored for compositional state-space analysis, applying a series of transformations to produce an equivalent model whose structure exhibits suitable modularity. In this thesis, we adopt Promela the as front-end language to automate refactoring. We select a subset of Promela and add some keywords for refactoring. The extended syntax is called rc-Promela, where “r” stands for “refactor” and “c” stands for “ccs.” We build a parser for rc-Promela, and use the parser to construct AST for rc-Promela model. Finally, we apply data flow analysis on AST to generate compact CCS state graphs for refactoring.
Automated finite-state verification techniques have matured considerably in the past decades, but state-space explosion remains an obstacle to their use. Theoretical lower bounds on complexity imply that all of the techniques that have been developed to avoid or mitigate state-space explosion depend on models that are “well-formed” in some way, and will usually fail for other models. This further implies that, when analysis is applied to models derived from designs or implementations of actual software systems, a model of the system “as built” is unlikely to be suitable for automated analysis. In particular, compositional hierarchical analysis (where state-space explosion is avoided by simplifying models of subsystems at several levels of abstraction) depends on the modular structure of the model to be analyzed. We describe how as-built finite-state models can be refactored for compositional state-space analysis, applying a series of transformations to produce an equivalent model whose structure exhibits suitable modularity. In this thesis, we adopt Promela the as front-end language to automate refactoring. We select a subset of Promela and add some keywords for refactoring. The extended syntax is called rc-Promela, where “r” stands for “refactor” and “c” stands for “ccs.” We build a parser for rc-Promela, and use the parser to construct AST for rc-Promela model. Finally, we apply data flow analysis on AST to generate compact CCS state graphs for refactoring.
Description
Keywords
組態爆炸, 局部性分析, 資料流分析, 自動驗證分析, state explosion, compositional analysis, data flow analysis, automatic verification