跳到主要內容

臺灣博碩士論文加值系統

(18.97.9.169) 您好!臺灣時間:2025/02/09 22:05
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果 :::

詳目顯示

我願授權國圖
: 
twitterline
研究生:賴輝陽
研究生(外文):Lai Huei Yang
論文名稱:以Estelle為敘述模式之漸進式壓縮多個體協定驗證系統
論文名稱(外文):A Reduced Incremental Protocol Verification System for N-Entity Estelle-Specified Protocols
指導教授:黃崇明黃崇明引用關係
指導教授(外文):Huang Chung Ming
學位類別:碩士
校院名稱:國立成功大學
系所名稱:資訊工程研究所
學門:工程學門
學類:電資工程學類
論文種類:學術論文
論文出版年:1993
畢業學年度:81
語文別:中文
論文頁數:181
中文關鍵詞:電腦網路協定工程協定驗證
外文關鍵詞:Computer NetworkProtocol EngineerProtocol Verification
相關次數:
  • 被引用被引用:0
  • 點閱點閱:103
  • 評分評分:
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
延伸的通信有限狀態機 (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 的架構、功能和實作方法。

By modifying Itoh and Ichikawa's CFSM-based reduction technique
and Huang et al.'s CFSM-based incremental verification
technique to be ECFSM-based, then integrating with Chu and Liu'
s ECFSM-based reduction techniques, this paper proposes a
protocol verification technique for ECFSM-based n-entity
protocols. Instead of executing one admissible event from a
global state to the other global state, the key part of Itoh
and Ichikawa's reduction technique is that all entities execute
one of their executable events parallelly from a global state
to the other global state. Chu and Liu's reduction technique is
based on the dead and live variables concept. Two global states
can be considered as equivalent when their dead variables'
values are different but live variables' values are equal.
Incremental verification allows adding or deleting transitions
at the run time of global state reachbility analysis. To
further reduce the number of global states which needs to be
checked, we integrate Chu and Liu's reduction technique with
Itoh and Ichikawa's reduction technique to have an ECFSM-based
reduced incremental protocol verification technique. In this
way, the integrated reduced incremental verification technique
can be directly applied to Estelle or SDL, which are ECFSM-
based FDTs, protocol verification systems. In this thesis, a
Reduced Incremental Estelle-based Protocol Verification System
(RIEPVS) which consists of an Estelle interpreter, a scheduler,
an incremental processing, and a graphic user interface (GUI)
has been developed based on the SUN OPENLOOK UNIX system. The
architecture, functionalities and implementation method of
RIEPVS are also presented in detail in this thesis.

QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top
無相關期刊