Browsing by Author "Chia-Yi Pan"

Filter results by typing the first few letters
Now showing 1 - 1 of 1
  • No Thumbnail Available
    Item
    一個PROMELA語法分析器並且運用資料流分析以產生簡潔的狀態圖
    (2003) 潘珈逸; Chia-Yi Pan
    近幾年來，自動驗證分析（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程式碼，以降低展開狀態圖之狀態空間，減少組態爆炸發生的可能性。