一個以派萃網路為基底之通訊協定核驗系統

Abstract

在網路系統日益發展下，通訊協定的設計漸漸地扮演著重要的角色，因而需要正規的 方法來有效地描述與核驗通訊協定。 在派萃網路基底之描述方法下，失們建立了一個通訊協定核驗系統，稱為ＰＮＡ（派 萃網路分析器）。在功能上，ＰＮＡ可以接受一個派萃網路圖，產生相對之可達檥（ reachabiliyt tree ），及對此樹進行多種分析。此外，如果一新的與舊的派萃網路 間的差異非常小時，ＰＮＡ可以經由舊的可達樹求得新皂可達檥。此種特性可以讓設 計者很有效率地改正其設計上小錯誤。再者，ＰＮＡ提供設計者可以經由系統之細化 功能對問題之芋一部份加以詳細描述或經由系統之抽象化功能對芋一部份加以簡化。 此種特性可以讓設計者以層次模組化飲方式來進行設計及核驗之工作。因此在適當的 使用ＰＮＡ下，一個通信協定之設計可以有效率地達成。