| 第1章 绪论 | 第1-12页 |
| ·课题的研究背景 | 第7-11页 |
| ·协议工程概述 | 第7-8页 |
| ·形式化模型技术概述 | 第8-9页 |
| ·形式描述技术 | 第9-10页 |
| ·Estelle技术概述 | 第10页 |
| ·研究形式化技术的意义 | 第10-11页 |
| ·课题的应用背景 | 第11-12页 |
| 第2章 有限状态机基础 | 第12-17页 |
| ·形式化模型技术概论 | 第12页 |
| ·经典有限状态机 | 第12-13页 |
| ·FSM的基本定义 | 第12页 |
| ·状态转移图 | 第12页 |
| ·非确定有限状态机 | 第12-13页 |
| ·有限状态机的简写形式 | 第13页 |
| ·带输出的有限状态机 | 第13-14页 |
| ·Moore机 | 第13-14页 |
| ·Mealy机 | 第14页 |
| ·扩展有限状态机 | 第14-15页 |
| ·传统状态机的不足 | 第14页 |
| ·扩展有限状态机 | 第14-15页 |
| ·状态机的本质 | 第15-17页 |
| ·状态 | 第15页 |
| ·扩展状态 | 第15页 |
| ·监测器 | 第15-16页 |
| ·事件 | 第16页 |
| ·动作和转换 | 第16页 |
| ·执行模型RTC | 第16-17页 |
| 第3章 形式描述技术 | 第17-21页 |
| ·形式化描述技术概论 | 第17页 |
| ·ESTELLE形式描述语言 | 第17-21页 |
| ·ESTELLE形式描述语言概述 | 第17-18页 |
| ·相关概念 | 第18-19页 |
| ·状态转换 | 第19-21页 |
| 第4章 基于VFNM的广播通道的描述 | 第21-28页 |
| ·Estelle通道描述的局限性 | 第21页 |
| ·广播通道扩展现状 | 第21页 |
| ·用多条通道来描述广播通道模型 | 第21-22页 |
| ·利用单独模块来描述广播通道模型 | 第22-23页 |
| ·C&A广播通道模型 | 第23-25页 |
| ·基于VFNM的扩展模型 | 第25-26页 |
| ·语法和语义 | 第26-27页 |
| ·广播通道语法修订 | 第26-27页 |
| ·广播通道的语义修订 | 第27页 |
| ·小结 | 第27-28页 |
| 第5章 TFTP协议分析 | 第28-32页 |
| ·TFTP协议概述 | 第28页 |
| ·TFTP协议与其他协议的关系 | 第28页 |
| ·TFTP的启动和终止 | 第28-29页 |
| ·TFTP的包格式 | 第29页 |
| ·TFTP的流量控制 | 第29页 |
| ·停止等待确认机制 | 第29-30页 |
| ·差错控制 | 第30页 |
| ·Sorcerer's Apprentice SyndromeScorer's问题 | 第30-31页 |
| ·数据包计数器 | 第31-32页 |
| 第6章 TFTP协议的有限状态机模型 | 第32-38页 |
| ·协议与有限状态机的对应关系 | 第32页 |
| ·事件的性质 | 第32页 |
| ·通道的FSM模型 | 第32-33页 |
| ·通道概念 | 第32-33页 |
| ·通道的状态化简 | 第33页 |
| ·TFTP通道的化简 | 第33页 |
| ·协议实体的FSM模型 | 第33-35页 |
| ·协议实体模型的化简 | 第33-34页 |
| ·TFTP协议的FSM模型 | 第34-35页 |
| ·TFTP协议FSM模型的改进 | 第35-38页 |
| ·协议改进方案的设计 | 第35-36页 |
| ·改进后的协议FSM模型 | 第36-38页 |
| 第7章 TFTP的ESTELLE描述 | 第38-41页 |
| ·TFTP的状态转换的描述 | 第38-39页 |
| ·TFTP的交互作用点和通道的定义 | 第39-40页 |
| ·TFTP的模块的定义 | 第40-41页 |
| 第8章 形式化综合技术 | 第41-43页 |
| 结论与展望 | 第43-44页 |
| 致谢 | 第44-45页 |
| 附录 | 第45-50页 |
| 附录Ⅰ TFTP协议说明 | 第45-46页 |
| 附录Ⅱ TFTP协议的Estelle描述 | 第46-50页 |
| 参考文献 | 第50-53页 |
| 已发论文 | 第53页 |