整合型高速網路軟體工程環境之研究與設計---高速網路通訊協定之實證與驗證(III)

Abstract

ATM在眾多高速網路中是最重要的一種，相對的設計與驗證ATM網路和其通訊協定也變成是是一件重要工作。運用傳統之網路和通訊協定的設計與分析方法來設計ATM通訊協定，其所得結果並不能完全滿足ATM通訊協定驗証的需求。因此，如何提供一個well-formed的規格語言，以及ATM高速網路性質的實證與驗證環境，無疑的是重要的工作。本計劃為整合計畫「整合性高速網路軟體工程環境之研究與設計」之一子計畫，為期三年，本研究為第三年。整體而言，第一年計劃之工作是提出適合描述ATM網路通訊協定規格描述語言。第二年的計畫目標在於定義ATM性質描述語言，以及提出一套驗證方法能夠驗證性質描述語言所描述之性質，驗證的方法包含以路徑導向為基礎的靜態驗證方與，以及以模擬為基礎的動態驗證方法，第二年進行後者。第三年的目標則在設計靜態驗證方法，以及將前兩年所設計的驗證方法製作成工具，並且與其它子計畫所設計的工具進行整合。第一年完成如下的工作：1.研究ATM高速網路之相關通訊協定重要的特性：2.加強Estelle的敘述能力使之適合ATM網路通訊協定的描述。3.建立一固定ATM網路的網路模擬程式在第二年度的計畫中，依照前一年度所提出的計畫書，本年度的工作目標在於研究ATM通訊協定軟體驗證的方法，以驗證ATM通訊協定所需具備的性質(擬定的方法包含具時間概念的路徑導向方法，以及以模擬為基礎的兩種驗證方法)。但是由於在第一年的計畫完成後，在年終檢討的時候，我們為了整體的計畫考量，將預定進行的工作修正為1. 研究與定義ATM通訊協定中所需驗證的性質，並以Temporal Logic為基礎設計依性質描述語言。2. 提出以模擬為基礎的驗證方法3. 利用一物件導向的分析設計方法設計模擬器與相關之模擬模型。4. 研究目前現有的以通訊協定正規驗證方法，與定義驗證所需要的驗證模型。5. 研究與設計物件導向通訊協定規格。6. 設計與製作ATM模擬器與以模擬為基礎的驗證環境在第三年的計畫中，我們則將致力於具時間概念的以路徑為基礎的驗證方法與相關環境的設計與製作。在驗證方法的研究上，我們將採用路徑導向的驗證方法突破”State SpaceExplosion Problem”，並且將之加入與時間有關的特性以及Temporal Logic的驗證能力。另外由於這將是計畫的最後一年我們將進行與其它子計畫所設計的系統進行整合。