基于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