【摘要】：如何實(shí)現(xiàn)腕表與智能手機(jī)之間低功耗和高可靠地傳輸計(jì)步數(shù)據(jù)是研發(fā)基于腕表的計(jì)步應(yīng)用系統(tǒng)必須解決的一個(gè)關(guān)鍵問(wèn)題。針對(duì)這個(gè)問(wèn)題,并充分考慮腕表受限的計(jì)算、存儲(chǔ)和供電能力,本文基于低功耗藍(lán)牙(BLE)設(shè)計(jì)了一種低功耗和高可靠的計(jì)步數(shù)據(jù)傳輸協(xié)議BLE-Step,并運(yùn)用體系結(jié)構(gòu)分析與設(shè)計(jì)語(yǔ)言AADL構(gòu)建了BLE-Step協(xié)議的體系結(jié)構(gòu)模型,進(jìn)一步運(yùn)用實(shí)時(shí)系統(tǒng)形式化驗(yàn)證工具UPPAAL開(kāi)展了對(duì)BLE-Step協(xié)議可靠性的形式化驗(yàn)證工作。本文的主要工作包括：(1)基于BLE4.0的應(yīng)用層協(xié)議規(guī)范,設(shè)計(jì)了一種用于腕表與智能手機(jī)之間進(jìn)行低功耗和高可靠傳輸?shù)挠?jì)步數(shù)據(jù)傳輸協(xié)議BLE-Step.在BLE-Step協(xié)議中定義了重傳服務(wù)、獲取數(shù)據(jù)塊信息列表服務(wù)與獲取特定計(jì)步數(shù)據(jù)塊服務(wù)共三種服務(wù)。在給出這些服務(wù)涉及的傳輸數(shù)據(jù)包的語(yǔ)法格式和語(yǔ)義解釋基礎(chǔ)上,定義了每種服務(wù)的行為及其協(xié)作過(guò)程。通過(guò)運(yùn)用BLE4.0技術(shù)并引入重傳服務(wù),較好地滿(mǎn)足腕表與智能手機(jī)之間低功耗和高可靠地傳輸計(jì)步數(shù)據(jù)的設(shè)計(jì)需求。(2)構(gòu)建了BLE-Step協(xié)議的AADL體系結(jié)構(gòu)模型。在BLE-Step協(xié)議的AADL模型中定義包括重傳、獲取數(shù)據(jù)塊信息列表與獲取特定計(jì)步數(shù)據(jù)塊共三種進(jìn)程構(gòu)件及其協(xié)作控制進(jìn)程構(gòu)件,給出了相關(guān)進(jìn)程構(gòu)件所傳輸數(shù)據(jù)包的數(shù)據(jù)構(gòu)件定義。并通過(guò)運(yùn)用AADL中的行為附件精確描述了各個(gè)進(jìn)程構(gòu)件中線(xiàn)程執(zhí)行的行為。構(gòu)建BLE-Step協(xié)議的AADL模型為實(shí)現(xiàn)對(duì)BLE-Step協(xié)議可靠性的形式化驗(yàn)證奠定基礎(chǔ)。(3)運(yùn)用UPPAAL形式化驗(yàn)證工具驗(yàn)證了BLE-Step協(xié)議的可靠性�；贐LE-Step協(xié)議的AADL模型,完成對(duì)BLE-Step協(xié)議中各個(gè)服務(wù)的時(shí)間自動(dòng)機(jī)模型建模及該協(xié)議服務(wù)過(guò)程的模擬。在給出BLE-Step協(xié)議的UPPAAL具體驗(yàn)證語(yǔ)法表達(dá)式的基礎(chǔ)上,最終運(yùn)用UPPAAL驗(yàn)證器完成對(duì)BLE-Step協(xié)議可靠性性質(zhì)的驗(yàn)證。形式化驗(yàn)證結(jié)果表明本文設(shè)計(jì)的BLE-Step協(xié)議是可靠的。本文設(shè)計(jì)的BLE-Step協(xié)議能夠滿(mǎn)足實(shí)際項(xiàng)目中低功耗高可靠的需求,現(xiàn)已成功運(yùn)用于商業(yè)產(chǎn)品中。同時(shí)該協(xié)議為設(shè)計(jì)基于藍(lán)牙低功耗傳輸其他數(shù)據(jù)的應(yīng)用層協(xié)議提供有用的借鑒與參考。
[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.
【學(xué)位授予單位】：福建師范大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2015
【分類(lèi)號(hào)】：TN925;TN915.04

【參考文獻(xiàn)】

相關(guān)期刊論文 前5條

1 劉倩;桂盛霖;李允;羅蕾;;基于UPPAAL的AADL模型可調(diào)度性驗(yàn)證[J];計(jì)算機(jī)應(yīng)用;2009年07期

2 楊志斌;皮磊;胡凱;顧宗華;馬殿富;;復(fù)雜嵌入式實(shí)時(shí)系統(tǒng)體系結(jié)構(gòu)設(shè)計(jì)與分析語(yǔ)言:AADL[J];軟件學(xué)報(bào);2010年05期

3 戴由旺;李增有;韋俞鋒;;基于ZigBee的低功耗無(wú)線(xiàn)傳感節(jié)點(diǎn)設(shè)計(jì)與實(shí)現(xiàn)[J];現(xiàn)代電子技術(shù);2011年18期

4 劉石;姚志強(qiáng);;基于ANT的無(wú)線(xiàn)溫度監(jiān)控系統(tǒng)設(shè)計(jì)[J];微型機(jī)與應(yīng)用;2013年02期

5 李立;朱秋君;單志林;李臻;;ANT低功耗無(wú)線(xiàn)網(wǎng)絡(luò)設(shè)計(jì)[J];物聯(lián)網(wǎng)技術(shù);2013年06期

相關(guān)碩士學(xué)位論文 前1條

1 李鑫;基于ZigBee生命體征監(jiān)測(cè)網(wǎng)絡(luò)的設(shè)計(jì)[D];哈爾濱理工大學(xué);2010年

，

本文編號(hào)：2175020