第三代行動通訊協定之正規化模型與驗證

這篇論文介紹如何應用正規化模型檢驗技術去驗證一個通訊協定的設計及實作。在我們的方法中，我們將每個協定層裡的元件經由嚴僅的驗證之後得到 "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.

並列關鍵字

TCTL ； Model checking ； Model checker ； RLC Layer ； Timed Automata

參考文獻

[3] ITU-T, Recommendation Z.100 (11/99) Specification and Description Language (SDL)

[4] R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and computation, 104, 2–34, 1993.

[5] R. Alur, D. Dill: "Automata for Modeling Real-time Systems", in Proceedings of ICALP90.

[7] R. E. Bryant. Graph-based algorithms for Boolean function manipulation. 1986

[8] R. E. Bryant. Symbolic Boolean manipulation with ordered binary decision diagrams.

國際替代計量

第三代行動通訊協定之正規化模型與驗證

全文下載

主題瀏覽