|
延伸的通信有限狀態機 (Extended Communication Finite State Machine, ECFSM) 模式是一種屬於狀態轉移模式 (State Transition Model) 的正式描述模式 (Formal Specification Model), 並且可以使用 與前後的文法有關係的變數 (Context Variable)和述語(Predicate) 來 對於用狀態轉移模式敘述的通信協定, 總體狀態分析 (Global State Reachability Analysis)是最直接的驗證方法之一。 據改進 Itoh 和 Ichikawa 之以 CFSM 為基礎的壓縮技術使其成為以 ECFSM 為基礎, 與 Chu 和 Liu 之以 ECFSM 為基礎的壓縮技術, 再加上改進 Huang 等人之 以通信有限狀態機為基礎的漸進式驗證技術 (Incremental Verification) 使其成為以 ECFSM 為基礎, 本論文提出一個針對多個體 ECFSM 為基礎之通信協定的壓縮漸進式驗證技術 (A Reduced Incremental Verification Technique)。Itoh 和 Ichikawa 之壓縮技術 的關鍵部份, 是在總體狀態分析中, 由一個總體狀態走到另一個總體狀態 時, 所有個體均平行地執行它們可執行的一個轉換, 取代在傳統上的總體 狀態分析中, 只能有一個個體執行它可執行的一個轉換。Chu 和 Liu 的 壓縮技術是以 dead-live 變數的觀念為基礎。當兩個總體狀態的 dead 變數不同但 live 變數相同時, 這兩個總體狀態可視為全等 (Equivalence)。而漸進式驗證是在做總體狀態分析時允許對被驗證的規 格做線上 (on-line) 增加或刪減一些轉換的動作, 然後根據修改的部 份, 對總體狀態分析做線上 (on-line) 適當的調整便可, 而不必從頭再 重新做一次總體狀態分析。為了進一步降低所需檢查之總體狀態的個數, 我們整合了 Chu 與 Liu 的壓縮技術、Itoh 與 Ichikawa 的壓縮技術和 Huang 等人的漸進式驗證技術, 而得到一個以 ECFSM 為基礎的漸進式協 定壓縮驗證技術。如此一來, 此整合的漸進式壓縮驗證技術能被直接應用 到如 Estelle 和 SDL 一樣的以ECFSM 為基礎之協定驗證系統。利用此一 新的驗證技術, 我們在 SUN OPENLOOK UNIX 系統上發展出來一套以 Estelle 為敘述模式之漸進式壓縮多個體協定驗證系統 (RIEPVS)。在 RIEPVS 中, 主要的子系統包括了 Estelle 的解譯程式 (Estelle Interpreter), 排程程式 (Scheduler), 漸進式處理 (Incremental Processing) 和圖形化的使用者介面 (Graphic User Interface, GUI)。 在此論文中, 我們也將詳細介紹 RIEPVS 的架構、功能和實作方法。
|