The Design And Verification Of A Profile For Step Data Transmission Based On Bluetooth Low Energy

How to deliver low power consumption and high reliable transmission of step data between the intelligent mobile phone and wrist-watch has been a key problem to be solved, in order to develop the step count application system based on wrist-watch. Aimed at the above problem and taking limited the Computation, storage and power supply capacity of watch into consideration fully, the paper designs a low-power and high reliable step counting data transmission profile based on BLE4.0 which named BLE-Step. And then, construct the system structure model of BLE-Step profile by Axiomatic Architecture Description Language (AADL). Finally, with the help of real time systems formal verification tool UPPAAL, carry out the work on formal verification of the reliability of BLE-Step Profile.The main listed as follows:(1) Based on application layer protocol specification of BLE4.0, design a low-power and high reliable step counting data transmission protocol which can transfer step counting data in Low power consumption and high reliable quality between wrist-watch and intelligent mobile phone. BLE-Step profile defines three service that include ReTranmitServices, BlockInfoListServices and StepDataByBlockServices. Defines the behavior and the collaboration process of each kind of service on basis of the syntax and semantic interpretation of the transmission data in those services.With the help of BLE4.0 and the retransmission, the profile satisfies the design requirements that step count data can be transfer in the low power consumption and high reliable quality between the watch and intelligent mobile phone(2) Construct the AADL models for BLE-Step profile. Model three services of the BLE-Step profile and feature attributes component in AADL system model and describe the behavior of these three kinds of service and synchronization control center accurately, which lay the foundation for the formal verification of the reliability of BLE-Step profile and prepare for the follow-up optimization of BLE-Step profile.(3) Use the UPPAAL formal verification tool to verify the reliability of BLE-Step profile. Model each service in BLE-Step profile by the timed automata model. Then, simulate the process behavior of profile. Finally verify the reliability of the profile by UPPAAL valuator. Formal verification results show that the proposed BLE-Step profile is reliable.The proposed BLE-Step profile can meet the needs of the real projects which need to transfer data in low power consumption and high reliable quality. And now, the profile has been successfully used in commercial products. At the same time, the profile can provide useful reference to design other application layer profile which based on BLE4.0.