Model Checking nRF24L01—based Internet of Things Systems

Jiamin Wang Milin Wang Kai Zheng Xin Huang

摘 要：PV energy system is concerned to solve pollution problems all over the world. Therefore， Internet of Things （IoT） is a monitoring network for PV system that based on the PV energy system to improve nRF24L01 system. This paper will analyze and improve the reliability of an nRF24L01 system by PRISM.

關(guān)鍵詞：Internet of things （IoT）； Model checking； Prism； Photovoltaic； nRF24L01； Raspberry Pi

I. INTRODUCTION AND SYSTEM DESIGN

Energy consumption problem becomes more concerned in various fields. In this paper， an nRF24L01 PV IoT system model is designed to analyze the reliability of the whole data-transmission system by PRISM.

In TABLE 1， compared with other two involved papers [1][2]， there are four points will be concerned in the experiment which are .improving reliability， and reducing calculation time， failure rate of one receiver， and the operation of sensor nodes and nRF24L01 wireless modules branches.

The architecture is displayed in Figure 1. Therefore， in the structure， there are five layers， and the main component is sensor node module.

Sensor node module： for the six different branches which contains different sensor nodes and nRF24L01 wireless module. Moreover， “l(fā)ambda_s” represents the failure rate of sensor nodes There is a sentence to check the reliability of the branches.

[] s1=1 -> s1*lambda_s ： （s1'=0）&（branch1'=0）；

Furthermore， there are two formulas which show the possible failure of system within 24 hours or 30 days.

“P=？ [ ！down U<=24*3600 ]”

“P=？ [ ！down U<=24*3600*30 ]”

II.EVALUATION AND IMPLEMENTATION

The graphs in Figure 2 show the impact of the nRF24L01 wireless models and sensors.

The curves in Figure 2 demonstrate that the failure probability decreases with the increases of the components.

III.CONCLUSION AND FUTURE WORK

In this paper， it is tempting to conclude that the reliability of the system depends on the failure rate of the components， and the duration. In future， the branches which include the sensor nodes and nRF24L01 wireless modules can be independent. Additionally， when data is transmitted， the structure can choose one optimal branch， which will be referred in future module analysis.

REFERENCES

[1]S. Wu， K. Zheng， and X. Huang， “Model Checking PV System with Remote Reprogramming Function，” Xian Jiaotong-Liverpool University， China.

[2]Y. Wang， X. Wu， K. Zheng， and X. Huang， ”Model Checking the Cloud-based IoT System with Reprogramming Function，” Department of Computer Science and Software Engineering Xian Jiaotong-Liverpool University， China.