基于UPPAAL的RFID定位系统准确性验证

来源：计算机技术与发展杂志2016年第09期北京时间：

作者：金仙力;陈楚娇

摘要：随着移动通信和移动定位技术的快速发展，极大地推动了移动目标定位系统的发展。对于移动目标实时定位需求的与日俱增，人们更加注重移动目标实时定位的准确性和可靠性。介绍了时间自动机理论，并分析了基于RFID技术的移动定位处理流程。采用时间自动机模型对移动定位系统进行形式化分析，分别对定位系统的四个核心模块—标签、阅读器、数据库和处理器进行建模。为了验证定位系统的可靠性，通过构建各个模块中的动作行为状态，判定不同行为状态之间的转换是否满足时间约束条件。采用模型检测工具UPPAAL对建模后的定位系统进行活性验证和安全性验证分析。实验结果表明：所设计的定位模型不存在死锁问题，满足系统的安全性并能确保移动目标的精确定位。

关键词：RFID定位系统;时间自动机;UPPAAL;模型验证