基于低功耗蓝牙的计步数据传输协议的设计与验证
发布时间：2018-08-09 19:09
【摘要】：如何实现腕表与智能手机之间低功耗和高可靠地传输计步数据是研发基于腕表的计步应用系统必须解决的一个关键问题。针对这个问题,并充分考虑腕表受限的计算、存储和供电能力,本文基于低功耗蓝牙(BLE)设计了一种低功耗和高可靠的计步数据传输协议BLE-Step,并运用体系结构分析与设计语言AADL构建了BLE-Step协议的体系结构模型,进一步运用实时系统形式化验证工具UPPAAL开展了对BLE-Step协议可靠性的形式化验证工作。本文的主要工作包括：(1)基于BLE4.0的应用层协议规范,设计了一种用于腕表与智能手机之间进行低功耗和高可靠传输的计步数据传输协议BLE-Step.在BLE-Step协议中定义了重传服务、获取数据块信息列表服务与获取特定计步数据块服务共三种服务。在给出这些服务涉及的传输数据包的语法格式和语义解释基础上,定义了每种服务的行为及其协作过程。通过运用BLE4.0技术并引入重传服务,较好地满足腕表与智能手机之间低功耗和高可靠地传输计步数据的设计需求。(2)构建了BLE-Step协议的AADL体系结构模型。在BLE-Step协议的AADL模型中定义包括重传、获取数据块信息列表与获取特定计步数据块共三种进程构件及其协作控制进程构件,给出了相关进程构件所传输数据包的数据构件定义。并通过运用AADL中的行为附件精确描述了各个进程构件中线程执行的行为。构建BLE-Step协议的AADL模型为实现对BLE-Step协议可靠性的形式化验证奠定基础。(3)运用UPPAAL形式化验证工具验证了BLE-Step协议的可靠性。基于BLE-Step协议的AADL模型,完成对BLE-Step协议中各个服务的时间自动机模型建模及该协议服务过程的模拟。在给出BLE-Step协议的UPPAAL具体验证语法表达式的基础上,最终运用UPPAAL验证器完成对BLE-Step协议可靠性性质的验证。形式化验证结果表明本文设计的BLE-Step协议是可靠的。本文设计的BLE-Step协议能够满足实际项目中低功耗高可靠的需求,现已成功运用于商业产品中。同时该协议为设计基于蓝牙低功耗传输其他数据的应用层协议提供有用的借鉴与参考。
[Abstract]:How to realize the low power consumption and high reliability transmission of step data between wrist watch and smart phone is a key problem that must be solved in the research and development of the application system based on wrist watch. Aiming at this problem, and fully considering the limited calculation, storage and power supply capacity of wrist watch, In this paper, a low power and high reliable step data transfer protocol (BLE-Step) is designed based on low power Bluetooth (BLE), and the architecture model of BLE-Step protocol is constructed by using the architecture analysis and design language AADL. Furthermore, the formal verification of the reliability of BLE-Step protocol is carried out by using the real-time system formal verification tool UPPAAL. The main work of this paper is as follows: (1) based on the application layer protocol specification of BLE4.0, a step data transfer protocol BLE-Stepfor low power consumption and high reliability transmission between wrist watch and smart phone is designed. The retransmission service is defined in the BLE-Step protocol. There are three services to obtain the data block information list service and the specific step data block service. Based on the syntax format and semantic explanation of the packets transmitted by these services, the behavior of each service and its cooperative process are defined. By using BLE4.0 technology and introducing retransmission service, the design requirements of low power consumption and high reliable transmission of step data between wrist watch and smart phone are well met. (2) the AADL architecture model of BLE-Step protocol is constructed. In the AADL model of BLE-Step protocol, there are three kinds of process components, including retransmission, obtaining the list of data blocks and obtaining the specific step data blocks, and the data component definitions of the data packets transmitted by the relevant process components are given. The behavior of thread execution in each process component is accurately described by using the behavior attachment in AADL. The construction of AADL model of BLE-Step protocol lays a foundation for formal verification of BLE-Step protocol reliability. (3) the reliability of BLE-Step protocol is verified by UPPAAL formal verification tool. Based on the AADL model of the BLE-Step protocol, the time automata model of each service in the BLE-Step protocol is modeled and the service process of the protocol is simulated. On the basis of giving the UPPAAL verification syntax expression of BLE-Step protocol, the reliability property of BLE-Step protocol is verified by using UPPAAL verifier. The formal verification results show that the BLE-Step protocol designed in this paper is reliable. The BLE-Step protocol designed in this paper can meet the requirements of low power consumption and high reliability in practical projects, and has been successfully applied to commercial products. At the same time, this protocol provides useful reference and reference for the design of application layer protocol based on Bluetooth low power transmission of other data.
【学位授予单位】：福建师范大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TN925;TN915.04
本文编号：2175020
[Abstract]:How to realize the low power consumption and high reliability transmission of step data between wrist watch and smart phone is a key problem that must be solved in the research and development of the application system based on wrist watch. Aiming at this problem, and fully considering the limited calculation, storage and power supply capacity of wrist watch, In this paper, a low power and high reliable step data transfer protocol (BLE-Step) is designed based on low power Bluetooth (BLE), and the architecture model of BLE-Step protocol is constructed by using the architecture analysis and design language AADL. Furthermore, the formal verification of the reliability of BLE-Step protocol is carried out by using the real-time system formal verification tool UPPAAL. The main work of this paper is as follows: (1) based on the application layer protocol specification of BLE4.0, a step data transfer protocol BLE-Stepfor low power consumption and high reliability transmission between wrist watch and smart phone is designed. The retransmission service is defined in the BLE-Step protocol. There are three services to obtain the data block information list service and the specific step data block service. Based on the syntax format and semantic explanation of the packets transmitted by these services, the behavior of each service and its cooperative process are defined. By using BLE4.0 technology and introducing retransmission service, the design requirements of low power consumption and high reliable transmission of step data between wrist watch and smart phone are well met. (2) the AADL architecture model of BLE-Step protocol is constructed. In the AADL model of BLE-Step protocol, there are three kinds of process components, including retransmission, obtaining the list of data blocks and obtaining the specific step data blocks, and the data component definitions of the data packets transmitted by the relevant process components are given. The behavior of thread execution in each process component is accurately described by using the behavior attachment in AADL. The construction of AADL model of BLE-Step protocol lays a foundation for formal verification of BLE-Step protocol reliability. (3) the reliability of BLE-Step protocol is verified by UPPAAL formal verification tool. Based on the AADL model of the BLE-Step protocol, the time automata model of each service in the BLE-Step protocol is modeled and the service process of the protocol is simulated. On the basis of giving the UPPAAL verification syntax expression of BLE-Step protocol, the reliability property of BLE-Step protocol is verified by using UPPAAL verifier. The formal verification results show that the BLE-Step protocol designed in this paper is reliable. The BLE-Step protocol designed in this paper can meet the requirements of low power consumption and high reliability in practical projects, and has been successfully applied to commercial products. At the same time, this protocol provides useful reference and reference for the design of application layer protocol based on Bluetooth low power transmission of other data.
【学位授予单位】：福建师范大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TN925;TN915.04
【参考文献】
相关期刊论文 前5条
1 刘倩;桂盛霖;李允;罗蕾;;基于UPPAAL的AADL模型可调度性验证[J];计算机应用;2009年07期
2 杨志斌;皮磊;胡凯;顾宗华;马殿富;;复杂嵌入式实时系统体系结构设计与分析语言:AADL[J];软件学报;2010年05期
3 戴由旺;李增有;韦俞锋;;基于ZigBee的低功耗无线传感节点设计与实现[J];现代电子技术;2011年18期
4 刘石;姚志强;;基于ANT的无线温度监控系统设计[J];微型机与应用;2013年02期
5 李立;朱秋君;单志林;李臻;;ANT低功耗无线网络设计[J];物联网技术;2013年06期
相关硕士学位论文 前1条
1 李鑫;基于ZigBee生命体征监测网络的设计[D];哈尔滨理工大学;2010年
，本文编号：2175020
本文链接：https://www.wllwen.com/kejilunwen/wltx/2175020.html
