中文摘要：

S-ALOHA协议是物联网RFID中决定标签信息能否及时可靠的被阅读器识别的关键技术之一,也是提高物联网服务质量的关键。实验,仿真和模拟主要通过探索S-ALOHA协议的部分行为对协议性质进行估算,得出的结论不具有精确性,本文采用一种高度自动化的形式化分析技术-概率模型检测完成S-ALOHA协议的精确分析。首先依据S-ALOHA的工作原理及特性,将其动态行为抽象成能支持非确定性,离散时间以及概率选择的马尔科夫决策过程,然后使用PRISM工具验证了模型的概率可达性和期望可达性,结果表明随着最大退避数的增加,S-ALOHA的期望时间比ALOHA的小6个时间单位,同时S-ALOHA发送数据的平均速度比ALOHA快1.2倍左右。

英文摘要：

In RFID Slotted - ALOHA （ S - ALOHA） is one of the key techniques which determine whether the information in the tag is identified by the reader timely and reliably, and is also a key technique improving the quality of service in Internet of Things. Experiment and simulation estimate the property by exploring the partial behavior of the S - ALOHA protocol such that the analysis is not accurate. In this paper we complete the precise analysis of the S - ALOHA protocol based on a high- ly automated formal analysis technology probabilistic model checking. First, based on the principle of S- ALOHA protocol, it＇s dynamic behavior is abstracted into a Markov Decision Process which can describe non -deterministic, discrete time and the probability selection. Then we use the PRISM tool to verify the model of probabilistic reachability and expected time. The result shows that with the increase of the value of maximum backoff, the value of expect time that occurred in S - ALOHA is smaller 6 units of time than ALOHA , and the average speed of the data transmission in S - ALOHA is 1.2 times faster than ALOHA.