基于时间着色Petri网的SIP协议形式化验证与分析
| 摘要 | 第1-6页 |
| ABSTRACT | 第6-8页 |
| 目录 | 第8-11页 |
| 第一章 引言 | 第11-14页 |
| ·研究背景 | 第11-12页 |
| ·研究内容和主要工作 | 第12页 |
| ·论文结构 | 第12-14页 |
| 第二章 背景知识 | 第14-26页 |
| ·SIP协议 | 第14-19页 |
| ·协议概述 | 第14-15页 |
| ·请求和响应分类 | 第15-16页 |
| ·呼叫方式 | 第16-19页 |
| ·CPN和CPN Tools | 第19-23页 |
| ·CPN的形式化定义 | 第19-20页 |
| ·层次CPN的形式化定义 | 第20-21页 |
| ·TCPN形式化定义 | 第21-23页 |
| ·正则表达式 | 第23-24页 |
| ·本章小结 | 第24-26页 |
| 第三章 SIP协议的形式化建模 | 第26-47页 |
| ·整体建模方法 | 第26-27页 |
| ·建模约束条件 | 第27-28页 |
| ·整体结构概述 | 第28-30页 |
| ·数据建模细节 | 第30-35页 |
| ·一般数据建模 | 第30-33页 |
| ·特殊数据建模 | 第33-35页 |
| ·product类数据 | 第33-34页 |
| ·Time类数据 | 第34-35页 |
| ·模型结构细节 | 第35-46页 |
| ·网络拓扑层 | 第35-36页 |
| ·状态变化层 | 第36-40页 |
| ·UAC和UAS端 | 第36-38页 |
| ·网络端 | 第38-40页 |
| ·实体行为层 | 第40-46页 |
| ·实体行为层结构 | 第40-41页 |
| ·定时器A的触发周期建模 | 第41-42页 |
| ·定时器触发事件建模 | 第42-43页 |
| ·消息处理建模 | 第43-44页 |
| ·同步处理方式 | 第44-45页 |
| ·与高层模型接口建模 | 第45-46页 |
| ·本章小结 | 第46-47页 |
| 第四章 SIP协议模型验证与分析 | 第47-61页 |
| ·SIP协议时间约束条件验证 | 第47-50页 |
| ·时间条件描述 | 第47-48页 |
| ·时间条件假设 | 第48页 |
| ·时间条件验证 | 第48-50页 |
| ·SIP协议模型验证与分析 | 第50-60页 |
| ·协议验证方法 | 第50页 |
| ·协议验证过程 | 第50-54页 |
| ·验证结果分析 | 第54-60页 |
| ·本章小结 | 第60-61页 |
| 第五章 SIP协议的改进 | 第61-73页 |
| ·死锁导致的可用性问题 | 第61页 |
| ·可用性问题解决方案 | 第61-64页 |
| ·方案1：UAC端处理 | 第62页 |
| ·方案2：UAS端处理 | 第62-64页 |
| ·方案3：C/S端共同处理 | 第64页 |
| ·解决方案验证 | 第64-70页 |
| ·UAC端方案验证 | 第65-67页 |
| ·UAS端方案验证 | 第67-69页 |
| ·C/S端共同解决方案验证 | 第69-70页 |
| ·方案对比 | 第70-72页 |
| ·本章小结 | 第72-73页 |
| 第六章 总结与展望 | 第73-75页 |
| ·总结 | 第73-74页 |
| ·进一步研究方向 | 第74-75页 |
| 参考文献 | 第75-78页 |
| 附录 | 第78-81页 |
| 致谢 | 第81页 |
