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

金仙力，陈楚娇

(南京邮电大学计算机学院软件学院，江苏南京 210003)

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

金仙力，陈楚娇

(南京邮电大学计算机学院软件学院，江苏南京 210003)

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

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

1 概述

随着移动通信技术、定位技术和RFID技术的不断发展，人们根据定位设备获取实时位置信息也越来越便捷，使得基于位置服务(Location Based Services，LBS)的系统得到了广泛应用。据统计，人类所获得的信息中80%以上的信息与位置(空间)有关。人类的生产活动和日常活动，都或多或少地涉及到位置信息，这极大地推动了移动目标定位系统的发展［1］。

目前，常用的移动目标定位方式主要是基于GPS的定位方法。……