一個PROMELA語法分析器並且運用資料流分析以產生簡潔的狀態圖

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.