随着移动通信和移动定位技术的快速发展，极大地推动了移动目标定位系统的发展。对于移动目标实时定位需求的与日俱增，人们更加注重移动目标实时定位的准确性和可靠性。介绍了时间自动机理论，并分析了基于RFID技术的移动定位处理流程。采用时间自动机模型对移动定位系统进行形式化分析，分别对定位系统的四个核心模块—标签、阅读器、数据库和处理器进行建模。为了验证定位系统的可靠性，通过构建各个模块中的动作行为状态，判定不同行为状态之间的转换是否满足时间约束条件。采用模型检测工具UPPAAL对建模后的定位系统进行活性验证和安全性验证分析。实验结果表明：所设计的定位模型不存在死锁问题，满足系统的安全性并能确保移动目标的精确定位。%Mobile positioning systems are greatly promoted with the rapid development of mobile communication and positioning technol-ogy. Due to the increasing demands of real-time moving targets positioning,the accuracy and reliability of real-time positioning for mov-ing target is paid more attention. The time automaton theory is introduced and the process of mobile positioning based on RFID technolo-gy is analyzed in this paper. The mobile positioning system is formally analyzed by time automaton model. Four core modules,including tag,reader,database and processor,are respectively modeled. In order to verify the reliability of positioning system,through the construc-tion of state action in each model,it makes sure whether the conversion between different decision behavior state can meet the time con-straints. Active authentication and security verification of positioning system are analyzed by checking tool UPPAAL. The experimental results show that the positioning model exists no deadlock problems,with enough safety and accuracy positioning of the moving target.
展开▼
