HCI协议的形式化描述、验证与实现
文献类型：学位论文
| 作者 | 蔡海龙 |
| 学位类别 | 博士 |
| 答辩日期 | 2000 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 中国科学院软件研究所 |
| 关键词 | 协议验证 自动代码生成 蓝牙 |
| 学位专业 | 计算机应用技术 |
| 中文摘要 | 随着网络技术的飞速发展，新的通信协议层出不穷。而目前协议软件的开发仍主要采用落后的阅读协议然后手工编码的方法，这样的协议软件开发方法不仅耗时较长，而且代码质量没有保障。本文采用了一种形式化的方法，即用SDL语言(Specification and Description Language)和MSC图(Message Sequence Chart)描述协议，并进行验证，最后从SDL模型自动生成C代码的开发方法。本文首先介绍一种最新的无线局域网通信协议——蓝牙(Bluetooth)协议。使用传统的方法开发此协议相当复杂而费时，因此我们考虑采用形式化方法，以求提高开发效率。接着，文章利用有限状态机的理论，详细讲述形式化的协议软件开发方法，重点介绍通过SDL和MSC进行描述、验证与代码生成的理论与应用，并对各种描述与验证方法进行比较。结合蓝牙协议中的HCI层和一种流行的软件开发工具包ObjectGeode，文章接下来给出了使用SDL和MSC对HCI协议进行描述、验证和代码生成的全过程，同时这也是一种较先进的通信协议软件开发流程。进行验证时，文章给出了仿真的结果以及错误分析，总结出协议验证的一些经验，并对各种协议验证方法的优据点进行探讨。与此同时，文章讨论了开发过程各阶段会遇到的一些相关问题以及解决办法。与传统的协议软件开发方法相比，这种开发方法不仅可以节省开发时间，而且可以通过开发过程中多次严格的验证提高代码的质量，因而在蓝牙协议软件的开发过程中发挥了重要作用。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 57 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/6432]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 蔡海龙. HCI协议的形式化描述、验证与实现[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2000. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。