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

金仙力，陈楚娇

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

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

金仙力，陈楚娇

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

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

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

1 概述

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

目前，常用的移动目标定位方式主要是基于GPS的定位方法。该方法能提供实时的位置、速度和高精度的时间信息。然而，随着物联网技术的飞速发展，其对传统的定位技术提出了新的要求。

随着人们对定位系统的返回结果的准确性要求越来越高，基于射频识别(Radio Frequency IDentification，RFID)的定位技术应运而生。RFID技术可以迅速准确地追踪目标并获得相关信息，实现不同物体在各种条件下的自动识别，免除了人工干涉，提高了信息处理速率。该技术的优点有:精度高、耐高温、不易磨损、寿命长、读取范围大、抗干扰强、操作方便、存储数据容量大，支持加密写入数据、可重复使用、可识别高速运动的物体、防止同时识别多个标签时的碰撞问题，适应环境能力强等［2-4］。运用RFID技术实现了短距离的定位以及室内的定位，室内的定位是GPS所不能解决的，所以文中采用RFID技术对移动目标进行定位。

完整的RFID系统一般包括标签(Tag)、阅读器(Reader)、后端数据库(Database)三部分，不同组件之间主要是通过信道来传递和交换消息的。由于各个信道之间信息传递具有顺序性，对RFID安全协议进行多次测试和行为模拟是确保其可靠性和安全性的两种常规方法［5］。

由R.Alur等提出的时间自动机是模拟和分析计算机科学领域中许多问题的有力工具，特别是在实时系统的模型验证中占据着重要的地位［6］。时间自动机模拟系统行为从而验证系统是否满足其规范的问题可以转化为验证两个自动机所接受的语言是否相互包含的问题［7］。这种先进行模型构造，然后再规范验证的方法将给系统设计者提供一种全新的系统分析方式。UPPAAL是一种以时间自动机作为行为模型的自动验证工具，已成功用于通信协议和实时系统的安全性分析［8］。

因此，为了验证基于RFID技术的定位系统的准确性和可靠性，文中采用UPPAAL时间自动机为建模工具，对基于RFID技术的定位系统中的核心进程进行模块化分析，并进行安全性问题验证。

2 相关理论

2.1 时间自动机理论

为了描述实时系统的时间约束，Alur等［9］提出了时间自动机理论。时间自动机在自动机的表达能力基础上，增加了对密集时间的描述能力，可用于对实时系统进行描述。

定义1(时间自动机):时间自动机是一个六元组(L，l0，C，A，E，I)。其中，L是位置集合;l0是初始位置;C是时钟集合;A是动作(包括协同动作和内部动作)集合;E∈L×A×B(C)×2C×L是从一个位置到另一个位置的边的集合，边上有动作、约束条件(guard)和时钟复位(clock reset)等条件;I是位置上的不变式。

定义2(时间自动机的语义):设(L，l0，C，A，E，I)是一个时间自动机，其语义可表示为一个标签转移系统 ＜S，s0，→＞。其中，S⊆L×RC是状态集合;s0= (l0，u0)是系统的初始状态;→⊆S×(R≥0∪A)×S表示如下的转移关系:-(l，u) →—d (l，u+d)。其中∀d＇:0≤d＇≤d⇒u+d＇∈I(l)。-(l，u) →—a (l＇，u＇)，其中e=(l，a，g，r，l＇)∈E使得u∈g，u＇=［r|→0］u，并且u＇∈I(l＇)，对于d∈R≥0，u+d把C中的每个时钟x映射为u(x)+d，［r|→0］u表示时钟值，其中r中的时钟被复位为0，C中其他时钟仍保持为u。

定义3(时间自动机网络的语义):设Ai=(Li，l0i，C，A，Ei，Ii)是时间自动机网络，=(l01，l02，…，l0n)是初始位置向量。Ai的语句可表示为标签转移系统小于S，s0，→＞。其中，S⊆(Li×…×Ln)×Rc是状态的集;s=(-l ，u);S×S 合000是系统初始状态→⊆ 表示转移关系，由以下规则定义:-(，u)(，u+d)。其中，∀d＇:0≤d＇≤d⇒u+d＇∈I()，-(，u)([ l ＇i/li]，u＇)，如果存在lil＇i，使得u∈g，u＇= [r →0]u，并且u＇∈I([ l ＇i/li])。-(，u)([ l ＇j/lj，l＇i/li]，u＇)，如果存在 li和 ljl＇j，使得u∈(gi∩gj)，u＇= [ri∪rj→0]u并且u＇∈I([ l＇j/lj，l＇i/li])。

2.2 自动验证工具UPPAAL

UPPAAL是由丹麦的Aalborg大学和瑞士的Uppsala大学于1995年联合开发，具有世界先进水平的实时系统模拟和验证工具［10］。它可以描述成非确定并行过程的系统。每个过程被描述为由有限控制结构、实数值时钟及变量组成的时间自动机。

UPPAAL采用基于时间自动机的模型描述语言。UPPAAL工具的建模语言基于时间自动机理论，同时又扩展了一些附加特性，比如有界整型变量(Bounded Integer Variable)和紧急度(Urgency)。它用时间自动机网络来表示系统模型。在UPPAAL中，系统被建模成由多个并行的时间自动机组成的自动机网络。建成的模型被进一步扩展使其带有有界离散变量，这些变量是状态的一部分。这些变量的用法就像程序设计语言那样:它们可读可写，并且服从一般的算术运算。系统的一个状态由所有自动机的位置，时间变量和离散变量的值定义。

UPPAAL工具的性质说明语言采用了 TCTL (Timed Computation Tree Logic，时间计算树逻辑)的一个子集。就像在TCTL中一样，这种性质说明语言包含两部分，一部分是路径公式，另一部分是状态公式。状态公式描述单独的状态，路径公式用来量化模型的路径或者路径的踪迹。路径公式可分为可达性、安全性和活性。UPPAAL支持几种不同的路径公式。其中，Α［］Φ表示所有路径中Φ都成立;Ε［］Φ表示存在一条路径，其上的所有状态中Φ都成立;Α［］Φ表示在所有路径中都存在Φ成立的状态;Ε［］Φ表示在某条路径中存在Φ成立的状态;Ψ→Φ表示若Ψ成立，则Φ最终也会成立。

采用UPPAAL工具进行安全性验证的案例广泛应用于多个领域。其中，包括从通信协议到多媒体应用、从实时系统到网络服务协议的多种类型的案例。常见的案例，如电源控制器的研究［11］、传送控制器的验证［12］、音频控制协议［13］、对WAP网关进行测试的研究［14］、网络服务的原子事务协议［15］和验证网络服务的业务活动协议［16］等。

3 基于时间自动机的系统建模

3.1 基于RFID安全协议的移动目标定位系统描述

文中设计的移动目标定位系统，主要采用RFID定位技术实现对移动对象的实时定位功能。为了便于多个移动定位操作的并发处理，在原有的RFID系统中设计处理器模块(Processor)，主要用于多个验证请求的并发处理，同时降低RFID阅读器和后台数据库之间的耦合性。具体定位过程分析如下:

(1)当电子标签进入阅读器的识别范围内，阅读器向其发送query消息请求认证。

(2)标签接收到阅读器的请求命令后，将metaID代替真实的标签ID发送给阅读器，其中metaID是hash函数映射标签密钥 key得来的，metaID=hash (key)，跟真实ID是对应存储在标签中。

(3)当阅读器收到metaID后发送给处理器。

(4)处理器将metaID发给数据库。

(5)由于后台应用系统的数据库存储了合法标签的ID、metaID、key，metaID也是由hash(key)得来。当后台应用系统收到处理器传输过来的metaID，查询数据库有没有与之对应的标签ID和key，如果有就将对应的标签ID和key通过处理器发送给阅读器，如果没有就发送认证失败的消息。

(6)阅读器收到处理器发送过来的标签ID与key后，保留标签ID，然后将key发送给电子标签。

(7)电子标签收到阅读器发送过来的key后利用hash函数运算该值，hash(key)，对比是否与自身存储的metaID值相同，如果相同就将标签ID发送给阅读器，如果不同就认证失败。

(8)阅读器收到标签发送过来的ID与后台应用系统传输过来的ID进行对比，相同则认证成功，否则认证失败。

(9)当验证成功后，阅读器向处理器发送rid(即阅读器唯一标识ID)。

(10)处理器将rid发送给数据库。

(11)数据库根据rid判断移动目标是进入(come)还是离开(leave)，并向处理器发送对应消息。

(12)处理器收到消息后向数据库发送相应的处理消息，更新位置信息(updatelocation)或者位置信息清空(null)。

3.2 基于UPPAAL的系统建模

根据系统的运行原理和相关描述，采用时间自动机模型对基于RFID的移动目标定位系统进行形式化设计建模。整个系统建立四个时间自动机模型，分别是tag(标签)时间自动机、processor(微机处理)时间自动机、reader(阅读器)时间自动机和database(数据库)时间自动机。它们之间通过前向和反向的信道通信，每个时间自动机加以时间约束。

(1)tag进程模板定义。

tag={L，l0，C，A，E，I};

L={tStart，tCheck，tIsSame，tIsMatchDkey，tMatchD-keyMid，tMatchDkey，tNotMatchDkey};

l0={tStart};

A={query，tmetaid，dkey，tid，nomatch2，wrong};

E∈L×A×B(C)×2C×L

标签进程tag在初始状态tStart从阅读器reader收到query认证请求消息后，转至状态tCheckId，之后发送消息tmetaid给reader，并转至状态tIsSame。当从reader收到wrong消息后，tag转至初始状态tStart;否则当从reader收到dkey消息后，验证metaID=H(key)是否成立。若不成立，转至状态tNotMatchDkey，并且tag向reader发送nomatch2消息，之后回到初始状态tStart;若成立，转至状态tMatchDkey，并且tag向reader发送tid消息，之后回到初始状态tStart。具体的标签进程模板如图1所示。

(2)reader进程模板定义。

reader={L，l0，C，A，E，I};

L={rStart，rCheckId，rCheckIdMid，rIsMatchId，rNotMatchKey，rMatcKeyId1，rIsMatchKey，rNotMatch-Key2，rNotMatchKeyIdMid，rMatchKey，rNotMatchKeyId，rNotMatchKeyIdMid，rIsMatchKeyId，rMatchKeyId，rMatchKeyIdid};

l0={rStart};

A={query，tmetaid，tmetaid1，fail，wrong，keyid1，dkey，tid，nomatch2，nomatchdkey，nomatchtid，rid};

E∈L×A×B(C)×2C×L

reader在初始状态rStart向tag发送query请求认证消息后，转至状态rCheckId，之后收到tag发来的tmetaid消息后，转至状态rCheckIdMid，然后向processor发送tmetaid1消息，转至状态 rIsMatchId;若收到processor的fail消息，则转至状态rNotMatchKey，并且向tag发送wrong消息，回到初始状态rStart;若收到processor发来的keyid1消息，则转至状态rMatchKey-Id1，然后向tag发送dkey消息，转至状态rIsMatchKey，此时若收到tag发来的nomatch2消息，那么向processor发送nomatchdkey消息，转至初始状态rStart，若收到的是tag发来的tid消息时，则要看tag发来的ID与processor发来的ID是否一致:如果不一致，那么转至状态rNotMatchKeyId，并向processor发送nomatchtid消息，回到初始状态rStart;如果一致，那么转至状态rMatchKeyId，并且向processor发送rid消息，回到初始状态rStart。具体的阅读器进程模板如图2所示。

(3)processor进程模板定义。

processor={L，l0，C，A，E，I};

L={pStart，pCheckId，pIsMatchId，pNotMatchId，pMatcKeyId，pIsMatchKeyId，pNotMatchKeyId，pNot-MatchKeyId，pMatchId，pSearch，pComeIn，pLeave};

l0={pStart};

A={tmetaid1，matchid，nomatchid，fail，keyid，keyid，nomatchtid，nomatchdkey，rid，search，leave，come，updatelocation，null};

E∈L×A×B(C)×2C×L

processor在初始状态 pStart收到 reader发来的tmetaid1消息后，转至状态pCheckId，之后向database发送matchid消息，转至状态pIsMatchId，若收到database发来的nomatchid消息，则转至状态pNotMatchId，然后向processor发送 fail的消息，并回到初始状态pStart;若收到的是database发来的keyid消息，转至状态pMatchKeyId，并向reader发送keyid1消息，转至状态pIsMatchKeyId，如果收到 reader发来的nomatchtid消息，那么回到初始状态pStart，如果收到reader发来的nomatchdkey消息，也回到初始状态pStart，如果收到reader发来的rid消息，则转至状态pMatchId，然后向database发送search消息，转至状态pSearch，此时若收到database发来的come消息，则转至状态pComeIn，并向database发送 updatelocation消息，回到初始状态pStart，若收到database发来的leave消息，则转至状态pLeave，并向database发送 null消息，回到初始状态pStart。具体的处理器进程模板如图3所示。

(4)database进程模板定义。

database={L，l0，C，A，E，I};

L={dStart，dCheckId，dIsMatchId，dNotMatchId，dMatcId，dNotMatchIdMid，dSearchregion，dComeOrLeave，dLeave，dLeaveMi，dCome，dComeMid};

l0={dStart};

A ={matched，keyed，nomatchid，search，leave，come，null，updatelocation};

E∈L×A×B(C)×2C×L

database在初始状态dStart收到processor发来的matchid消息，转至状态dCheckId，并查询自己的数据库是否存在与metaID匹配的项，若找到，转至状态dMatchId，之后向processor发送keyid消息，回到初始状态dStart;若未找到，转至状态dNotMatchId，之后向processor发送nomatchid消息，并回到初始状态dStart。如果ID卡验证成功，则会收到processor发来的search消息，转至状态dSearchregion，若是外阅读器，则转至状态dLeave，并向processor发送leave消息，转至状态dLeaveMid，之后收到processor发来的null消息，回到初始状态dStart;若是内读写器，则转至状态dCome，并向processor发送come消息，转至状态dComeMid，之后收到processor发来的updatelocation消息，回到初始状态dStart。具体的数据库进程模板如4所示。

4 使用UPPAAL对模型进行验证

用UPPAAL的模拟器对上述模块进行模拟时，随机得到一个各实体之间通过管道相互通信、控制的消息序列。具体多个组件间的通信流程如图5所示。

从图中可见，初步判定模型符合系统要求。对模型进行分析后，下面对系统的性能进行验证，最重要的就是避免死锁的产生，所以必须在UPPAAL的验证器中验证以下查询语言。

4.1 系统活性和安全性验证分析

针对系统的活性验证，满足属性A［］not deadlock，可以表明系统在运行过程中没有出现死锁。针对系统的安全性验证，主要从以下几个属性进行判断:

(1)A［］database.dNotMatchId+database.dMatchId＜=1，表明database的metaID与tag的metaID不一致时，database会向处理器发送不匹配的消息(nomatchid)，即认证失败;否则向处理器发送真实ID和key值，继续后续的认证。

(2)A［］tag.tNotMatchDkey+tag.tMatchDkey＜=1，表明database的key值应用hash函数(hash(key))得到的metaID与tag保存的metaID不一致时，tag会向reader发送不匹配的消息(nomatch2)，即认证失败;否则向reader发送自己的真实ID，继续后续的认证。

(3)A［］reader.rMatchKeyId+reader.rNotMatchKeyId ＜=1，表明tag发来的真实ID与database发来的metaID不一致时，向处理器发送不匹配消息(nomatchtid)，即认证失败;否则向处理器发送匹配消息(rid)，继续后续对移动目标的定位。

4.2 系统精确性验证分析

(1)E＜＞(database.dComeMid and processor. pComeIn)，表明当reader的唯一位置ID判断为外阅读器时，此时移动目标是进入管理区域，处理器触发数据库更新目标对象位置信息。

(2)E＜＞(database.dLeaveMid and processor. pLeave)，表明当reader的唯一位置ID判断为内阅读器时，此时移动目标是离开管理区域，处理器触发数据库清空目标对象的位置信息。

4.3 验证结果

根据4.1节中属性A［］not deadlock结果可知，系统满足活性验证，运行中不会出现死锁现象。根据4.1节中的验证结果(1)、(2)和(3)可知，系统满足安全性。根据4.2节中的验证结果(1)和(2)可知，系统满足定位的精确性。具体验证结果如图6所示。

5 结束语

文中通过形式化方法模型检测语言，采用UPPAAL建模工具对基于RFID技术的移动目标定位系统中标签、阅读器、处理器和后台数据库四个核心模块进行建模，并从系统活性、安全性和定位精确性方面进行验证分析。由验证结果可知，所设计的移动目标系统能够满足安全性以及对移动目标进行精确定位。文中仅对系统层面的设计进行了验证，下一步是对模块的验证。

［1］ 史 悦.基于RFID的移动目标跟踪系统研究与设计［D］.成都:电子科技大学，2010.

［2］ 丁振华，李锦涛，冯 波.基于Hash函数的RFID安全认证协议研究［J］.计算机研究与发展，2009，46(4):583-592.

［3］ 游战清，戴青云，陈 涛，等.无线射频识别系统安全指南［M］.北京:电子工业出版社，2007.

［4］ 杜治国，杨 波，欧阳国帧，等.安全的RFID认证协议研究设计［J］.计算机工程和设计，2009，30(3):561-565.

［5］ 陈彦君.RFID系统安全协议的研究［D］.南京:南京邮电大学，2013.

［6］ Springintveld J，Vaandrager F，D’Argenio P R.Testing timed automata［J］.Theoretical Computer Science，1997，254(1): 225-257.

［7］ Bozga M，Maler O，Pnueli A，et al.Some progress in the symbolic verification of timed automata［J］.Lecture Notes in Computer Science，1997，1254:179-190.

［8］ 周清雷，王 静，赵东明.UPPAAL环境下通讯协议的自动验证［J］.河南师范大学学报:自然科学版，2006，34(4):40 -42.

［9］ Alur R，Dill D L.A theory of timed automata［J］.Theoretical Computer Science，1994，126(2):183-235.

［10］Behrmann G，David A，Larsen K G.A tutorial on UPPAAL 4.0 ［R］.Denmark:Aalborg University，2006.

［11］Havelund K，Larsen K G，Skou A.Formal verification of a power controller using the real-time model checker UPPAAL［J］. Lecture Notes in Computer Science，1999，1601:277-298.

［12］Lindahl M，Pettersson P，Yi W.Formal design and analysis of a gear controller［J］.International Journal on Software Tools for Technology Transfer，2001，3(3):353-368.

［13］Bengtsson J，David G W O，Kristoffersen K J，et al.Automated verification of an audio-control protocol using UPPAAL［J］. The Journal of Logic and Algebraic Programming，2002，52-53:163-181.

［14］Hessel A，Pettersson P.Model-based testing of a WAP gateway:an industrial case-study［C］//Proceedings of the 11th international workshop，FMICS 2006 and 5th international workshop，PDMC conference on formal methods:applications and technology.［s.l.］:Springer-Verlag，2006:116-131.

［15］Ravn A P，Srba J，Vighio S.A formal analysis of the web services atomic transaction protocol with UPPAAL［J］.Lecture Notes in Computer Science，2010，6415:579-593.

［16］Ravn A P，Srba J，Vighio S.Modelling and verification of web services business activity protocol［J］.Lecture Notes in Computer Science，2011，6605:357-371.

Accuracy Verification of RFID Positioning System Based on UPPAAL

JIN Xian-li，CHEN Chu-jiao
(School of Computer Science and Technology，School of Software，Nanjing University of Posts and Telecommunications，Nanjing 210003，China)

Mobile positioning systems are greatly promoted with the rapid development of mobile communication and positioning technology.Due to the increasing demands of real-time moving targets positioning，the accuracy and reliability of real-time positioning for moving target is paid more attention.The time automaton theory is introduced and the process of mobile positioning based on RFID technology 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 construction of state action in each model，it makes sure whether the conversion between different decision behavior state can meet the time constraints. 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.

RFID positioning system;time automaton;UPPAAL;model validation

TP393

A

1673-629X(2016)09-0104-05

10.3969/j.issn.1673-629X.2016.09.024

2015-11-17

2016-02-24< class="emphasis_bold">网络出版时间:

时间:2016-08-01

国家自然科学基金资助项目(61373139)

金仙力(1978-)，男，博士，副教授，研究方向为形式化方法、Web服务和信息安全等;陈楚娇(1989-)，女，硕士生，研究方向为RFID定位和模型认证等。

http://www.cnki.net/kcms/detail/61.1450.TP.20160801.0909.064.html