臺灣博碩士論文加值系統

通訊程序的複雜度因需求的增加而不斷地提高, 分析通訊程序的問題愈來愈困難。本
論文提出同步與非同步通訊有限狀態機綱路的Pumping 定理, 並應用這些pumping 定
理於分析通訊程序的方法中, 同時提出所需分析reachability tree 高度的上限。實
驗結果顯示pumping 現象非常普遍與實際, 且死結(deadlocks) 和未定義接收(unsp-
ecified receptions) 都能在reachability tree 高度上限之內被偵測出來。
我們的主要結果及貢獻摘要如下:
(1) 導出同步通訊有限狀態機綱路的pumping 定理。
(2) 證明兩個同步通訊有限狀態機綱路分析的時間複雜度上限為O(mn(m+n)k+mnk4),
其中m 和n 分別是兩個同步通訊有限狀態機的狀態數目,k是訊息型態的數目。
(3) 提出一個分析同步通訊程序的簡式Petri 綱路分析法。
(4) 導出非同步通訊有限狀態機綱路的pumping 定理。
(5) 提出一個分析非同步通訊有限狀態機綱路的pumping-based 方法。此方法提出一
個分析reachability tree 時的高度上限Cm(m-1)2︱Σ︱, 其中C 是混合乘積中最大
可能向外邊(outgoing edges)數目,m是混合乘積的狀態數目, ︱Σ︱是訊息型態的數
目。
(6) 當reachability tree 分析到Cm(m-1)2︱Σ︱高度時, 若所有可繼續分析的分支
均合pumping 定理, 則此通訊程序的nonprogress 問題為decidable。
(7) 提出對應於pumping 定理的topology解釋。

目次
中文摘要
圖目錄
表目錄
第一章 緒論
1.1 通訊程序分析與動機
1.2 窮舉式可達性分析法
1.3 有限狀態機的抽運輔助定理
1.4 本論文的主要目標
1.5 為何採用抽運定理
1.6 論文結構
第二章 相關研究
2.1 通訊程序的模型
2.2 通訊程序分析的研究
2.3 可決定性
2.4 本章摘要
第三章 同步通訊程序分析
3.1 同步通訊程序分析與分支測試
3.2 同步通訊程序模型與抽運定理
3.3 循序軟體的測試與分析方法之不適用
3.4 並行執行流
3.5 路徑選擇
3.6 品質指標與預算限制
3.7 例子與實驗
3.8 本章摘要
第四章 非同步通訊有限狀態機網路與抽運定理
4.1 非同步通訊程序分析與FSM的抽運 輔助定理
4.2 非同步通訊有限狀態機及基本定義
4.3 非同步通訊有限狀態機網路的抽運定理
4.4 本章摘要
第五章 非同步通訊程序分析
5.1 以抽運定理為基礎之分析方法
5.2 抽運定理應用在偵測死結和未定義接收
5.3 一個非同步通訊有限狀態機網路分析的新方法
5.4 實驗與比較
5.5 本章摘要
第六章 非同步程序分析的決定性
6.1 佇列中的重複訊息和全等全體狀態
6.2 佇列重複訊息分析
6.3 分析非同步通訊有限狀態機網路可達性樹高度上限
6.4 比較
6.5 本章摘要
第七章 結論與展望
參考文獻
附錄 實驗所用非同步通訊有限狀態機網路