(3.238.7.202) 您好!臺灣時間:2021/03/01 21:11
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果

詳目顯示:::

我願授權國圖
: 
twitterline
研究生:朱良鈞
研究生(外文):Chu, Liang-Jung
論文名稱:使用模型檢驗器SPIN測試與驗證並行程式
論文名稱(外文):Test and Verification of Concurrent Programs Using the Model Checker SPIN
指導教授:黃廷祿
指導教授(外文):Ting-Lu Huang
學位類別:碩士
校院名稱:國立交通大學
系所名稱:資訊工程學系
學門:工程學門
學類:電資工程學類
論文種類:學術論文
論文出版年:1998
畢業學年度:86
語文別:中文
論文頁數:60
中文關鍵詞:模型檢驗狀態劇增問題
外文關鍵詞:Model checkingstate explosion
相關次數:
  • 被引用被引用:0
  • 點閱點閱:206
  • 評分評分:系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
針對硬體的驗證工作,模型檢驗(model checking)已被證明是一項十
分成功的技術。我們以實例說明如何使用模型檢驗器(model checker)
SPIN測試與驗證並行程式(concurrent program)。首先,我們使用SPIN尋
找出兩個已刊載的互斥程式(mutual exclusion algorithm)的錯誤。將這
種傑出的找錯能力應用到情節方法(scenario approach)上,對於程式,
我們將獲得更多有關各組成要素的了解。接著,我們使用SPIN協助發展並
行程式。模型檢驗中的主要難題稱為狀態劇增問題(state explosion
problem)。我們所提出用以解決狀態劇增的方法,是利用SPIN的特性以及
對目標程式所擁有的知識。最後,根據我們的試驗,我們要鼓勵軟體設計
者使用模型檢驗器,將它視為偵錯及驗證工作的輔助工具。

Model checking is a proven successful technology for verifying
hardware. We demonstrate how model checking can be used to test
and verify concurrent programs with the model checker SPIN.
First, we use SPIN to find subtle errors in two published mutual
exclusion algorithms. By applying this outstanding capability of
finding errors to a scenario approach, we would gain a
component-wise understanding of the target program. Then, we use
SPIN to help develop concurrent programs. The main problem in
model checking is the state explosion problem. Our approach to
attacking state explosion exploits the nature of SPIN and the
knowledge of the target program. Finally, according to our
experiment we intend to encourage software designers to use a
model checker as a tool in both debugging and verification.

QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top
系統版面圖檔 系統版面圖檔