協定驗證分析器-使用加上時間的可到達分析方法

Abstract

一． 緒論 1.1 正規化技術的需求 1.2 PVA 系統的需求 1.3 現有的方法與限制 1.4 研究動機 1.5 論文組織 二． 協定描述模型與可到達分析 2.1 研究背景 2.2 定義 2.3 克服可到達分析的爆炸問題 2.3.1 使用受限種類的加時模型減少全面狀態記錄所需的記憶數 2.3.2 消除由並行事件排序所引起的爆炸問題 三． 協定可到達狀態產生器╱有效驗證器 3.1 順序程式的觀念性並行處理與數學式時間位置圖表示法 3.2 協定可到達狀態產生╱有效驗證演算法 3.2.1 監督程序 3.2.2 轉移程序 3.3 演算法的執行舉例 3.4 協定有效驗證 3.5 實驗結果與討論 3.5.1 實驗結果 3.5.2 討論 四． 協定循環性驗證與績效分析 4.1 協定性質與定義 4.2 協定循環性驗證演算法 4.3 實驗結果與績效分析 4.3.1 實驗結果 4.3.2 績效分析 五． 結論 5.1 結論 5.2 未來研究工作