王凡臺灣大學：電機工程學研究所王建銘Wang, Jian-MingJian-MingWang2007-11-262018-07-062007-11-262018-07-062004http://ntur.lib.ntu.edu.tw//handle/246246/53343這篇論文介紹如何應用正規化模型檢驗技術去驗證一個通訊協定的設計及實作。在我們的方法中，我們將每個協定層裡的元件經由嚴僅的驗證之後得到 "Golden Formal Model"，這些模組將可以被重覆的在設計中使用，並且利用來驗證其他待測的協定、實作好的元件。 因為正規化驗證在現代的驗證技術中具有重要的地位，因此這篇論文的架構將在第二章先介紹正規化驗證的理論背景，並且強調在模型檢驗方面的介紹。第三章簡介第三代行動通訊協定層，主要強調 RLC Layer 的介紹。第四章介紹我們實驗所使用的工具 Red，並且強調在釐清時間自動機的概念及TCTL公式的使用方法。第五章介紹一些用以建立 Golden Formal Model 的策略，並且強調在抽象化的層次對於效能的影響，並且列出一些簡單的 Golden Formal Model 的狀態圖以及建立時所使用的概念。第六章我們建立了 Specification Properties Library，如同於 Golden Formal Model 的概念，Golden Formal Model有一些不變的特性，如果Golden Formal Model被其他設計所使用或替代，SPL裡所對應的規則將可以重覆的被使用，我們在此也簡單的介紹一些規則。最後我們給了一個簡單的結論，說明這些方法的重要性。This thesis introduces how formal verification technology is used in the protocol software design included protocol design and implementation. We aim at developing a set of golden formal models for protocol software. The set of models can then be used in several ways to help engineers simulating, testing, emulating, and synthesizing various designs. We first discuss our general framework in using these golden models. Then we gave an overview for formal verification using model-checking. Finally, we give some strategies to modeling and abstracting the system. We use Red, which is a model-checker/simulator for real-time systems, to check the correctness and precision of our golden models.Table of Contents Chapter 1 Introduction - 1- 1.1 Rapid growth in telecommunication - 1 - 1.2 The thirst for reliable systems - 3 - 1.3 Dependable methodology for system validation - 4 - Chapter 2 Formal verification－MODEL-CHECKING - 5 - 2.1 Models - 6 - 2.2 Description and specification languages - 9 - 2.3 State-explosion problem and performance issue - 13 - Chapter 3 The overview of RLC protocol - 14 - 3.1 Modes of RLC - 14 - 3.2 Primitives of RLC - 21 - 3.3 Protocol states of RLC - 23 - Chapter 4 Formal modeling of telecommunication system with Red - 31 - 4.1 Modeling - 32 - 4.2 Specification - 39 - Chapter 5 Verification framework - 44 - 5.1 The experiment platform with Red - 44 - 5.2 Rules for modeling and abstracting - 46 - 5.3 The golden formal model of RLC UM entities - 53 - Chapter 6 Specification properties library (SPL) - 59 - Chapter 7 Experiment result and analysis - 61 - Chapter 8 Conclusion - 63 - Bibliography - 64 -2095054 bytesapplication/pdfen-US時間自動機模型檢驗模型檢驗工具TCTLModel checkingModel checkerRLC LayerTimed Automatathesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/53343/1/ntu-93-R91921051-1.pdf