基于Color Petri Nets的HMIPv6协议形式化验证研究

文摘

英文文摘

图表目录

第1章 引 言

1.1 研究背景

1.2 国内外研究现状

1.3 研究内容和主要工作

1.4 论文结构

第2章 背景知识

2.1 HMIPv6协议简介

2.2 CPN和CPNTOOLS简介

2.3 本章小结

第3章 HMIPv6协议属性提取

3.1 HMIPv6协议(RFC5380)分析方法

3.1.1 基于事件的设计方法

3.1.2 协议属性提取方法

3.2 协议属性提取

3.2.1 事件行为属性

3.2.2 状态

3.2.3 数据类型

3.2.4 协议属性描述

3.3 本章小结

第4章 模型建立

4.1 CPN模型的抽象层次

4.2 建模约束条件

4.3 数据建模

4.4“通用模块”设计思想

4.5 CPN层次化建模

4.5.1 TOP层建模

4.6 本章小结

第5章 模型的验证

5.1 模型验证方法

5.2 宏移动功能单元验证

5.3 微移动功能单元验证

5.4 隧道功能单元验证

5.5 功能单元并发情况验证

5.6 本章小结

第6章 结束语

6.1 总结

6.2 进一步工作

参考文献

致谢