Formal modeling and verification of a Third Generation Mobile Communication Protocol
Date Issued
2004
Date
2004
Author(s)
Wang, Jian-Ming
DOI
zh-TW
Abstract
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.
Subjects
時間自動機
模型檢驗
模型檢驗工具
TCTL
Model checking
Model checker
RLC Layer
Timed Automata
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-93-R91921051-1.pdf
Size
23.31 KB
Format
Adobe PDF
Checksum
(MD5):f5a6d5bc3974b1af61c9152be8b975ad