|
通訊程序的複雜度因需求的增加而不斷地提高, 分析通訊程序的問題愈來愈困難。本 論文提出同步與非同步通訊有限狀態機綱路的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解釋。
|