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

dc.contributor鄭永斌zh_TW
dc.contributorYung-Ping Chengen_US
dc.contributor.author潘珈逸zh_TW
dc.contributor.authorChia-Yi Panen_US
dc.date.accessioned2019-08-29T07:44:45Z
dc.date.available2003-7-10
dc.date.available2019-08-29T07:44:45Z
dc.date.issued2003
dc.description.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程式碼,以降低展開狀態圖之狀態空間,減少組態爆炸發生的可能性。zh_TW
dc.description.abstractAutomated 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.en_US
dc.description.sponsorship資訊教育研究所zh_TW
dc.identifierG0069008016
dc.identifier.urihttp://etds.lib.ntnu.edu.tw/cgi-bin/gs32/gsweb.cgi?o=dstdcdr&s=id=%22G0069008016%22.&%22.id.&
dc.identifier.urihttp://rportal.lib.ntnu.edu.tw:80/handle/20.500.12235/92646
dc.language英文
dc.subject組態爆炸zh_TW
dc.subject局部性分析zh_TW
dc.subject資料流分析zh_TW
dc.subject自動驗證分析zh_TW
dc.subjectstate explosionen_US
dc.subjectcompositional analysisen_US
dc.subjectdata flow analysisen_US
dc.subjectautomatic verificationen_US
dc.title一個PROMELA語法分析器並且運用資料流分析以產生簡潔的狀態圖zh_TW
dc.titleAn Extended PROMELA Parser Which Generates Compact CCS State Graphs Using Data Flow Analysis for Refactoring Automationen_US

Files

Original bundle
Now showing 1 - 5 of 9
No Thumbnail Available
Name:
801601.pdf
Size:
25.19 KB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
801602.pdf
Size:
76.3 KB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
801603.pdf
Size:
84.16 KB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
801604.pdf
Size:
34.07 KB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
801605.pdf
Size:
43.1 KB
Format:
Adobe Portable Document Format

Collections