中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
HCI协议的形式化描述、验证与实现
作者: 蔡海龙
答辩日期: 2000
专业: 计算机应用技术
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 协议验证 ; 自动代码生成 ; 蓝牙
摘要: 随着网络技术的飞速发展,新的通信协议层出不穷。而目前协议软件的开发仍主要采用落后的阅读协议然后手工编码的方法,这样的协议软件开发方法不仅耗时较长,而且代码质量没有保障。本文采用了一种形式化的方法,即用SDL语言(Specification and Description Language)和MSC图(Message Sequence Chart)描述协议,并进行验证,最后从SDL模型自动生成C代码的开发方法。本文首先介绍一种最新的无线局域网通信协议——蓝牙(Bluetooth)协议。使用传统的方法开发此协议相当复杂而费时,因此我们考虑采用形式化方法,以求提高开发效率。接着,文章利用有限状态机的理论,详细讲述形式化的协议软件开发方法,重点介绍通过SDL和MSC进行描述、验证与代码生成的理论与应用,并对各种描述与验证方法进行比较。结合蓝牙协议中的HCI层和一种流行的软件开发工具包ObjectGeode,文章接下来给出了使用SDL和MSC对HCI协议进行描述、验证和代码生成的全过程,同时这也是一种较先进的通信协议软件开发流程。进行验证时,文章给出了仿真的结果以及错误分析,总结出协议验证的一些经验,并对各种协议验证方法的优据点进行探讨。与此同时,文章讨论了开发过程各阶段会遇到的一些相关问题以及解决办法。与传统的协议软件开发方法相比,这种开发方法不仅可以节省开发时间,而且可以通过开发过程中多次严格的验证提高代码的质量,因而在蓝牙协议软件的开发过程中发挥了重要作用。
英文摘要: With the rapid development of network technology, new communication protocols emerge endlessly. But as for the development of protocol software, the old method still in use is reading protocol specification and then coding manually, which is time consuming and cannot ensure good quality of source code. In this article, a formal method is adopted to specify protocol by SDL, validate it and generate C code from SDL model. This paper firstly introduces a new wireless communication protocol used in local areas, Bluetooth. Since using traditional way to develop the new protocol software is very complicated and time consuming, the formal method is considered and adopted to improve its efficiency. Then the theory of FSM_Finite State Machine) is used in this paper to explain the formal method of developing protocol software. Theories and applications are analyzed in detail on specifying, validating and code generation with SDL and MSC. And some specific methods of specification and validation are compared. Through the actual development of HCI layer in Bluetooth protocol suite with a very popular software developing tools package, ObjectGeode from Verilog, this paper illustrates how to specify, validate protocols in SDL and MSC and generate source code from SDL. This process also shows an advanced workflow of protocol software development. During the validation, this paper presents the result and analysis of simulation and summarizes some experiences of protocol validation. The advantages and disadvantages of these validating methods are discussed as well. At the same time, some problems and possible solutions are discussed. Compared with traditional ways, this method of development can reduce developing time and improve the code quality dramatically, and plays an important role in the development of Bluetooth protocol software.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6432
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
LW002152.pdf(2240KB)----限制开放-- 联系获取全文

Recommended Citation:
蔡海龙. HCI协议的形式化描述、验证与实现[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2000-01-01.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[蔡海龙]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[蔡海龙]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace