| 摘要 | 第4-5页 |
| Abstract | 第5页 |
| 1 绪论 | 第8-13页 |
| 1.1 论文的选题背景和研究意义 | 第8-10页 |
| 1.2 国内外研究现状 | 第10-11页 |
| 1.3 论文的主要研究内容 | 第11-13页 |
| 2 Timed RAISE形式化方法 | 第13-23页 |
| 2.1 Timed RAISE背景及其特点 | 第13-14页 |
| 2.2 Timed RAISE标准语言 | 第14-19页 |
| 2.2.1 RSL基本概念 | 第14-16页 |
| 2.2.2 RSL中的操作符 | 第16-18页 |
| 2.2.3 时间因子的引入 | 第18-19页 |
| 2.3 RSL建模与验证方法 | 第19-20页 |
| 2.4 RSL开发工具与推理规则 | 第20-23页 |
| 2.4.1 RSL开发工具 | 第20-21页 |
| 2.4.2 RSL的推理规则 | 第21-23页 |
| 3 基于Timed RAISE的RBC切换协议的模型构建 | 第23-41页 |
| 3.1 RBC切换 | 第23-28页 |
| 3.1.1 RBC切换流程分析 | 第23-26页 |
| 3.1.2 交互信息图的构建 | 第26-28页 |
| 3.2 RBC切换协议状态转移图的构建 | 第28-31页 |
| 3.2.1 域的建模方法 | 第28-29页 |
| 3.2.2 状态转移图的构建 | 第29-31页 |
| 3.3 RBC切换协议RSL模型的构建 | 第31-41页 |
| 3.3.1 双电台工作时RSL模型 | 第32-38页 |
| 3.3.2 单电台工作时RSL模型 | 第38-41页 |
| 4 RBC切换协议的模型验证 | 第41-48页 |
| 4.1 双电台工作时的模型验证 | 第41-45页 |
| 4.2 单电台工作时的模型验证 | 第45-46页 |
| 4.3 验证结果分析 | 第46-48页 |
| 结论 | 第48-49页 |
| 致谢 | 第49-50页 |
| 参考文献 | 第50-53页 |
| 附录A RBC切换的RSL模型 | 第53-69页 |
| 攻读学位期间的研究成果 | 第69页 |