基于UPPAAL的RFID定位系統(tǒng)準(zhǔn)確性驗證

金仙力，陳楚嬌

(南京郵電大學(xué)計算機(jī)學(xué)院軟件學(xué)院，江蘇南京 210003)

基于UPPAAL的RFID定位系統(tǒng)準(zhǔn)確性驗證

金仙力，陳楚嬌

(南京郵電大學(xué)計算機(jī)學(xué)院軟件學(xué)院，江蘇南京 210003)

隨著移動通信和移動定位技術(shù)的快速發(fā)展，極大地推動了移動目標(biāo)定位系統(tǒng)的發(fā)展。對于移動目標(biāo)實時定位需求的與日俱增，人們更加注重移動目標(biāo)實時定位的準(zhǔn)確性和可靠性。介紹了時間自動機(jī)理論，并分析了基于RFID技術(shù)的移動定位處理流程。采用時間自動機(jī)模型對移動定位系統(tǒng)進(jìn)行形式化分析，分別對定位系統(tǒng)的四個核心模塊—標(biāo)簽、閱讀器、數(shù)據(jù)庫和處理器進(jìn)行建模。為了驗證定位系統(tǒng)的可靠性，通過構(gòu)建各個模塊中的動作行為狀態(tài)，判定不同行為狀態(tài)之間的轉(zhuǎn)換是否滿足時間約束條件。采用模型檢測工具UPPAAL對建模后的定位系統(tǒng)進(jìn)行活性驗證和安全性驗證分析。實驗結(jié)果表明:所設(shè)計的定位模型不存在死鎖問題，滿足系統(tǒng)的安全性并能確保移動目標(biāo)的精確定位。

RFID定位系統(tǒng);時間自動機(jī);UPPAAL;模型驗證

1 概述

隨著移動通信技術(shù)、定位技術(shù)和RFID技術(shù)的不斷發(fā)展，人們根據(jù)定位設(shè)備獲取實時位置信息也越來越便捷，使得基于位置服務(wù)(Location Based Services，LBS)的系統(tǒng)得到了廣泛應(yīng)用。據(jù)統(tǒng)計，人類所獲得的信息中80%以上的信息與位置(空間)有關(guān)。人類的生產(chǎn)活動和日常活動，都或多或少地涉及到位置信息，這極大地推動了移動目標(biāo)定位系統(tǒng)的發(fā)展［1］。

目前，常用的移動目標(biāo)定位方式主要是基于GPS的定位方法。該方法能提供實時的位置、速度和高精度的時間信息。然而，隨著物聯(lián)網(wǎng)技術(shù)的飛速發(fā)展，其對傳統(tǒng)的定位技術(shù)提出了新的要求。

隨著人們對定位系統(tǒng)的返回結(jié)果的準(zhǔn)確性要求越來越高，基于射頻識別(Radio Frequency IDentification，RFID)的定位技術(shù)應(yīng)運(yùn)而生。RFID技術(shù)可以迅速準(zhǔn)確地追蹤目標(biāo)并獲得相關(guān)信息，實現(xiàn)不同物體在各種條件下的自動識別，免除了人工干涉，提高了信息處理速率。該技術(shù)的優(yōu)點有:精度高、耐高溫、不易磨損、壽命長、讀取范圍大、抗干擾強(qiáng)、操作方便、存儲數(shù)據(jù)容量大，支持加密寫入數(shù)據(jù)、可重復(fù)使用、可識別高速運(yùn)動的物體、防止同時識別多個標(biāo)簽時的碰撞問題，適應(yīng)環(huán)境能力強(qiáng)等［2-4］。運(yùn)用RFID技術(shù)實現(xiàn)了短距離的定位以及室內(nèi)的定位，室內(nèi)的定位是GPS所不能解決的，所以文中采用RFID技術(shù)對移動目標(biāo)進(jìn)行定位。

完整的RFID系統(tǒng)一般包括標(biāo)簽(Tag)、閱讀器(Reader)、后端數(shù)據(jù)庫(Database)三部分，不同組件之間主要是通過信道來傳遞和交換消息的。由于各個信道之間信息傳遞具有順序性，對RFID安全協(xié)議進(jìn)行多次測試和行為模擬是確保其可靠性和安全性的兩種常規(guī)方法［5］。

由R.Alur等提出的時間自動機(jī)是模擬和分析計算機(jī)科學(xué)領(lǐng)域中許多問題的有力工具，特別是在實時系統(tǒng)的模型驗證中占據(jù)著重要的地位［6］。時間自動機(jī)模擬系統(tǒng)行為從而驗證系統(tǒng)是否滿足其規(guī)范的問題可以轉(zhuǎn)化為驗證兩個自動機(jī)所接受的語言是否相互包含的問題［7］。這種先進(jìn)行模型構(gòu)造，然后再規(guī)范驗證的方法將給系統(tǒng)設(shè)計者提供一種全新的系統(tǒng)分析方式。UPPAAL是一種以時間自動機(jī)作為行為模型的自動驗證工具，已成功用于通信協(xié)議和實時系統(tǒng)的安全性分析［8］。

因此，為了驗證基于RFID技術(shù)的定位系統(tǒng)的準(zhǔn)確性和可靠性，文中采用UPPAAL時間自動機(jī)為建模工具，對基于RFID技術(shù)的定位系統(tǒng)中的核心進(jìn)程進(jìn)行模塊化分析，并進(jìn)行安全性問題驗證。

2 相關(guān)理論

2.1 時間自動機(jī)理論

為了描述實時系統(tǒng)的時間約束，Alur等［9］提出了時間自動機(jī)理論。時間自動機(jī)在自動機(jī)的表達(dá)能力基礎(chǔ)上，增加了對密集時間的描述能力，可用于對實時系統(tǒng)進(jìn)行描述。

定義1(時間自動機(jī)):時間自動機(jī)是一個六元組(L，l0，C，A，E，I)。其中，L是位置集合;l0是初始位置;C是時鐘集合;A是動作(包括協(xié)同動作和內(nèi)部動作)集合;E∈L×A×B(C)×2C×L是從一個位置到另一個位置的邊的集合，邊上有動作、約束條件(guard)和時鐘復(fù)位(clock reset)等條件;I是位置上的不變式。

定義2(時間自動機(jī)的語義):設(shè)(L，l0，C，A，E，I)是一個時間自動機(jī)，其語義可表示為一個標(biāo)簽轉(zhuǎn)移系統(tǒng) ＜S，s0，→＞。其中，S?L×RC是狀態(tài)集合;s0= (l0，u0)是系統(tǒng)的初始狀態(tài);→?S×(R≥0∪A)×S表示如下的轉(zhuǎn)移關(guān)系:-(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中的時鐘被復(fù)位為0，C中其他時鐘仍保持為u。

定義3(時間自動機(jī)網(wǎng)絡(luò)的語義):設(shè)Ai=(Li，l0i，C，A，Ei，Ii)是時間自動機(jī)網(wǎng)絡(luò)，=(l01，l02，…，l0n)是初始位置向量。Ai的語句可表示為標(biāo)簽轉(zhuǎn)移系統(tǒng)小于S，s0，→＞。其中，S?(Li×…×Ln)×Rc是狀態(tài)的集;s=(-l ，u);S×S 合000是系統(tǒng)初始狀態(tài)→? 表示轉(zhuǎn)移關(guān)系，由以下規(guī)則定義:-(，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大學(xué)和瑞士的Uppsala大學(xué)于1995年聯(lián)合開發(fā)，具有世界先進(jìn)水平的實時系統(tǒng)模擬和驗證工具［10］。它可以描述成非確定并行過程的系統(tǒng)。每個過程被描述為由有限控制結(jié)構(gòu)、實數(shù)值時鐘及變量組成的時間自動機(jī)。

UPPAAL采用基于時間自動機(jī)的模型描述語言。UPPAAL工具的建模語言基于時間自動機(jī)理論，同時又?jǐn)U展了一些附加特性，比如有界整型變量(Bounded Integer Variable)和緊急度(Urgency)。它用時間自動機(jī)網(wǎng)絡(luò)來表示系統(tǒng)模型。在UPPAAL中，系統(tǒng)被建模成由多個并行的時間自動機(jī)組成的自動機(jī)網(wǎng)絡(luò)。建成的模型被進(jìn)一步擴(kuò)展使其帶有有界離散變量，這些變量是狀態(tài)的一部分。這些變量的用法就像程序設(shè)計語言那樣:它們可讀可寫，并且服從一般的算術(shù)運(yùn)算。系統(tǒng)的一個狀態(tài)由所有自動機(jī)的位置，時間變量和離散變量的值定義。

UPPAAL工具的性質(zhì)說明語言采用了 TCTL (Timed Computation Tree Logic，時間計算樹邏輯)的一個子集。就像在TCTL中一樣，這種性質(zhì)說明語言包含兩部分，一部分是路徑公式，另一部分是狀態(tài)公式。狀態(tài)公式描述單獨的狀態(tài)，路徑公式用來量化模型的路徑或者路徑的蹤跡。路徑公式可分為可達(dá)性、安全性和活性。UPPAAL支持幾種不同的路徑公式。其中，Α［］Φ表示所有路徑中Φ都成立;Ε［］Φ表示存在一條路徑，其上的所有狀態(tài)中Φ都成立;?。郏荭当硎驹谒新窂街卸即嬖讦党闪⒌臓顟B(tài);Ε［］Φ表示在某條路徑中存在Φ成立的狀態(tài);Ψ→Φ表示若Ψ成立，則Φ最終也會成立。

采用UPPAAL工具進(jìn)行安全性驗證的案例廣泛應(yīng)用于多個領(lǐng)域。其中，包括從通信協(xié)議到多媒體應(yīng)用、從實時系統(tǒng)到網(wǎng)絡(luò)服務(wù)協(xié)議的多種類型的案例。常見的案例，如電源控制器的研究［11］、傳送控制器的驗證［12］、音頻控制協(xié)議［13］、對WAP網(wǎng)關(guān)進(jìn)行測試的研究［14］、網(wǎng)絡(luò)服務(wù)的原子事務(wù)協(xié)議［15］和驗證網(wǎng)絡(luò)服務(wù)的業(yè)務(wù)活動協(xié)議［16］等。

3 基于時間自動機(jī)的系統(tǒng)建模

3.1 基于RFID安全協(xié)議的移動目標(biāo)定位系統(tǒng)描述

文中設(shè)計的移動目標(biāo)定位系統(tǒng)，主要采用RFID定位技術(shù)實現(xiàn)對移動對象的實時定位功能。為了便于多個移動定位操作的并發(fā)處理，在原有的RFID系統(tǒng)中設(shè)計處理器模塊(Processor)，主要用于多個驗證請求的并發(fā)處理，同時降低RFID閱讀器和后臺數(shù)據(jù)庫之間的耦合性。具體定位過程分析如下:

(1)當(dāng)電子標(biāo)簽進(jìn)入閱讀器的識別范圍內(nèi)，閱讀器向其發(fā)送query消息請求認(rèn)證。

(2)標(biāo)簽接收到閱讀器的請求命令后，將metaID代替真實的標(biāo)簽ID發(fā)送給閱讀器，其中metaID是hash函數(shù)映射標(biāo)簽密鑰 key得來的，metaID=hash (key)，跟真實ID是對應(yīng)存儲在標(biāo)簽中。

(3)當(dāng)閱讀器收到metaID后發(fā)送給處理器。

(4)處理器將metaID發(fā)給數(shù)據(jù)庫。

(5)由于后臺應(yīng)用系統(tǒng)的數(shù)據(jù)庫存儲了合法標(biāo)簽的ID、metaID、key，metaID也是由hash(key)得來。當(dāng)后臺應(yīng)用系統(tǒng)收到處理器傳輸過來的metaID，查詢數(shù)據(jù)庫有沒有與之對應(yīng)的標(biāo)簽ID和key，如果有就將對應(yīng)的標(biāo)簽ID和key通過處理器發(fā)送給閱讀器，如果沒有就發(fā)送認(rèn)證失敗的消息。

(6)閱讀器收到處理器發(fā)送過來的標(biāo)簽ID與key后，保留標(biāo)簽ID，然后將key發(fā)送給電子標(biāo)簽。

(7)電子標(biāo)簽收到閱讀器發(fā)送過來的key后利用hash函數(shù)運(yùn)算該值，hash(key)，對比是否與自身存儲的metaID值相同，如果相同就將標(biāo)簽ID發(fā)送給閱讀器，如果不同就認(rèn)證失敗。

(8)閱讀器收到標(biāo)簽發(fā)送過來的ID與后臺應(yīng)用系統(tǒng)傳輸過來的ID進(jìn)行對比，相同則認(rèn)證成功，否則認(rèn)證失敗。

(9)當(dāng)驗證成功后，閱讀器向處理器發(fā)送rid(即閱讀器唯一標(biāo)識ID)。

(10)處理器將rid發(fā)送給數(shù)據(jù)庫。

(11)數(shù)據(jù)庫根據(jù)rid判斷移動目標(biāo)是進(jìn)入(come)還是離開(leave)，并向處理器發(fā)送對應(yīng)消息。

(12)處理器收到消息后向數(shù)據(jù)庫發(fā)送相應(yīng)的處理消息，更新位置信息(updatelocation)或者位置信息清空(null)。

3.2 基于UPPAAL的系統(tǒng)建模

根據(jù)系統(tǒng)的運(yùn)行原理和相關(guān)描述，采用時間自動機(jī)模型對基于RFID的移動目標(biāo)定位系統(tǒng)進(jìn)行形式化設(shè)計建模。整個系統(tǒng)建立四個時間自動機(jī)模型，分別是tag(標(biāo)簽)時間自動機(jī)、processor(微機(jī)處理)時間自動機(jī)、reader(閱讀器)時間自動機(jī)和database(數(shù)據(jù)庫)時間自動機(jī)。它們之間通過前向和反向的信道通信，每個時間自動機(jī)加以時間約束。

(1)tag進(jìn)程模板定義。

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

標(biāo)簽進(jìn)程tag在初始狀態(tài)tStart從閱讀器reader收到query認(rèn)證請求消息后，轉(zhuǎn)至狀態(tài)tCheckId，之后發(fā)送消息tmetaid給reader，并轉(zhuǎn)至狀態(tài)tIsSame。當(dāng)從reader收到wrong消息后，tag轉(zhuǎn)至初始狀態(tài)tStart;否則當(dāng)從reader收到dkey消息后，驗證metaID=H(key)是否成立。若不成立，轉(zhuǎn)至狀態(tài)tNotMatchDkey，并且tag向reader發(fā)送nomatch2消息，之后回到初始狀態(tài)tStart;若成立，轉(zhuǎn)至狀態(tài)tMatchDkey，并且tag向reader發(fā)送tid消息，之后回到初始狀態(tài)tStart。具體的標(biāo)簽進(jìn)程模板如圖1所示。

(2)reader進(jìn)程模板定義。

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在初始狀態(tài)rStart向tag發(fā)送query請求認(rèn)證消息后，轉(zhuǎn)至狀態(tài)rCheckId，之后收到tag發(fā)來的tmetaid消息后，轉(zhuǎn)至狀態(tài)rCheckIdMid，然后向processor發(fā)送tmetaid1消息，轉(zhuǎn)至狀態(tài) rIsMatchId;若收到processor的fail消息，則轉(zhuǎn)至狀態(tài)rNotMatchKey，并且向tag發(fā)送wrong消息，回到初始狀態(tài)rStart;若收到processor發(fā)來的keyid1消息，則轉(zhuǎn)至狀態(tài)rMatchKey-Id1，然后向tag發(fā)送dkey消息，轉(zhuǎn)至狀態(tài)rIsMatchKey，此時若收到tag發(fā)來的nomatch2消息，那么向processor發(fā)送nomatchdkey消息，轉(zhuǎn)至初始狀態(tài)rStart，若收到的是tag發(fā)來的tid消息時，則要看tag發(fā)來的ID與processor發(fā)來的ID是否一致:如果不一致，那么轉(zhuǎn)至狀態(tài)rNotMatchKeyId，并向processor發(fā)送nomatchtid消息，回到初始狀態(tài)rStart;如果一致，那么轉(zhuǎn)至狀態(tài)rMatchKeyId，并且向processor發(fā)送rid消息，回到初始狀態(tài)rStart。具體的閱讀器進(jìn)程模板如圖2所示。

(3)processor進(jìn)程模板定義。

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在初始狀態(tài) pStart收到 reader發(fā)來的tmetaid1消息后，轉(zhuǎn)至狀態(tài)pCheckId，之后向database發(fā)送matchid消息，轉(zhuǎn)至狀態(tài)pIsMatchId，若收到database發(fā)來的nomatchid消息，則轉(zhuǎn)至狀態(tài)pNotMatchId，然后向processor發(fā)送 fail的消息，并回到初始狀態(tài)pStart;若收到的是database發(fā)來的keyid消息，轉(zhuǎn)至狀態(tài)pMatchKeyId，并向reader發(fā)送keyid1消息，轉(zhuǎn)至狀態(tài)pIsMatchKeyId，如果收到 reader發(fā)來的nomatchtid消息，那么回到初始狀態(tài)pStart，如果收到reader發(fā)來的nomatchdkey消息，也回到初始狀態(tài)pStart，如果收到reader發(fā)來的rid消息，則轉(zhuǎn)至狀態(tài)pMatchId，然后向database發(fā)送search消息，轉(zhuǎn)至狀態(tài)pSearch，此時若收到database發(fā)來的come消息，則轉(zhuǎn)至狀態(tài)pComeIn，并向database發(fā)送 updatelocation消息，回到初始狀態(tài)pStart，若收到database發(fā)來的leave消息，則轉(zhuǎn)至狀態(tài)pLeave，并向database發(fā)送 null消息，回到初始狀態(tài)pStart。具體的處理器進(jìn)程模板如圖3所示。

(4)database進(jìn)程模板定義。

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在初始狀態(tài)dStart收到processor發(fā)來的matchid消息，轉(zhuǎn)至狀態(tài)dCheckId，并查詢自己的數(shù)據(jù)庫是否存在與metaID匹配的項，若找到，轉(zhuǎn)至狀態(tài)dMatchId，之后向processor發(fā)送keyid消息，回到初始狀態(tài)dStart;若未找到，轉(zhuǎn)至狀態(tài)dNotMatchId，之后向processor發(fā)送nomatchid消息，并回到初始狀態(tài)dStart。如果ID卡驗證成功，則會收到processor發(fā)來的search消息，轉(zhuǎn)至狀態(tài)dSearchregion，若是外閱讀器，則轉(zhuǎn)至狀態(tài)dLeave，并向processor發(fā)送leave消息，轉(zhuǎn)至狀態(tài)dLeaveMid，之后收到processor發(fā)來的null消息，回到初始狀態(tài)dStart;若是內(nèi)讀寫器，則轉(zhuǎn)至狀態(tài)dCome，并向processor發(fā)送come消息，轉(zhuǎn)至狀態(tài)dComeMid，之后收到processor發(fā)來的updatelocation消息，回到初始狀態(tài)dStart。具體的數(shù)據(jù)庫進(jìn)程模板如4所示。

4 使用UPPAAL對模型進(jìn)行驗證

用UPPAAL的模擬器對上述模塊進(jìn)行模擬時，隨機(jī)得到一個各實體之間通過管道相互通信、控制的消息序列。具體多個組件間的通信流程如圖5所示。

從圖中可見，初步判定模型符合系統(tǒng)要求。對模型進(jìn)行分析后，下面對系統(tǒng)的性能進(jìn)行驗證，最重要的就是避免死鎖的產(chǎn)生，所以必須在UPPAAL的驗證器中驗證以下查詢語言。

4.1 系統(tǒng)活性和安全性驗證分析

針對系統(tǒng)的活性驗證，滿足屬性A［］not deadlock，可以表明系統(tǒng)在運(yùn)行過程中沒有出現(xiàn)死鎖。針對系統(tǒng)的安全性驗證，主要從以下幾個屬性進(jìn)行判斷:

(1)A［］database.dNotMatchId+database.dMatchId＜=1，表明database的metaID與tag的metaID不一致時，database會向處理器發(fā)送不匹配的消息(nomatchid)，即認(rèn)證失敗;否則向處理器發(fā)送真實ID和key值，繼續(xù)后續(xù)的認(rèn)證。

(2)A［］tag.tNotMatchDkey+tag.tMatchDkey＜=1，表明database的key值應(yīng)用hash函數(shù)(hash(key))得到的metaID與tag保存的metaID不一致時，tag會向reader發(fā)送不匹配的消息(nomatch2)，即認(rèn)證失敗;否則向reader發(fā)送自己的真實ID，繼續(xù)后續(xù)的認(rèn)證。

(3)A［］reader.rMatchKeyId+reader.rNotMatchKeyId ＜=1，表明tag發(fā)來的真實ID與database發(fā)來的metaID不一致時，向處理器發(fā)送不匹配消息(nomatchtid)，即認(rèn)證失敗;否則向處理器發(fā)送匹配消息(rid)，繼續(xù)后續(xù)對移動目標(biāo)的定位。

4.2 系統(tǒng)精確性驗證分析

(1)E＜＞(database.dComeMid and processor. pComeIn)，表明當(dāng)reader的唯一位置ID判斷為外閱讀器時，此時移動目標(biāo)是進(jìn)入管理區(qū)域，處理器觸發(fā)數(shù)據(jù)庫更新目標(biāo)對象位置信息。

(2)E＜＞(database.dLeaveMid and processor. pLeave)，表明當(dāng)reader的唯一位置ID判斷為內(nèi)閱讀器時，此時移動目標(biāo)是離開管理區(qū)域，處理器觸發(fā)數(shù)據(jù)庫清空目標(biāo)對象的位置信息。

4.3 驗證結(jié)果

根據(jù)4.1節(jié)中屬性A［］not deadlock結(jié)果可知，系統(tǒng)滿足活性驗證，運(yùn)行中不會出現(xiàn)死鎖現(xiàn)象。根據(jù)4.1節(jié)中的驗證結(jié)果(1)、(2)和(3)可知，系統(tǒng)滿足安全性。根據(jù)4.2節(jié)中的驗證結(jié)果(1)和(2)可知，系統(tǒng)滿足定位的精確性。具體驗證結(jié)果如圖6所示。

5 結(jié)束語

文中通過形式化方法模型檢測語言，采用UPPAAL建模工具對基于RFID技術(shù)的移動目標(biāo)定位系統(tǒng)中標(biāo)簽、閱讀器、處理器和后臺數(shù)據(jù)庫四個核心模塊進(jìn)行建模，并從系統(tǒng)活性、安全性和定位精確性方面進(jìn)行驗證分析。由驗證結(jié)果可知，所設(shè)計的移動目標(biāo)系統(tǒng)能夠滿足安全性以及對移動目標(biāo)進(jìn)行精確定位。文中僅對系統(tǒng)層面的設(shè)計進(jìn)行了驗證，下一步是對模塊的驗證。

［1］ 史 悅.基于RFID的移動目標(biāo)跟蹤系統(tǒng)研究與設(shè)計［D］.成都:電子科技大學(xué)，2010.

［2］ 丁振華，李錦濤，馮 波.基于Hash函數(shù)的RFID安全認(rèn)證協(xié)議研究［J］.計算機(jī)研究與發(fā)展，2009，46(4):583-592.

［3］ 游戰(zhàn)清，戴青云，陳 濤，等.無線射頻識別系統(tǒng)安全指南［M］.北京:電子工業(yè)出版社，2007.

［4］ 杜治國，楊 波，歐陽國幀，等.安全的RFID認(rèn)證協(xié)議研究設(shè)計［J］.計算機(jī)工程和設(shè)計，2009，30(3):561-565.

［5］ 陳彥君.RFID系統(tǒng)安全協(xié)議的研究［D］.南京:南京郵電大學(xué)，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環(huán)境下通訊協(xié)議的自動驗證［J］.河南師范大學(xué)學(xué)報:自然科學(xué)版，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，F(xiàn)MICS 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">網(wǎng)絡(luò)出版時間:

時間:2016-08-01

國家自然科學(xué)基金資助項目(61373139)

金仙力(1978-)，男，博士，副教授，研究方向為形式化方法、Web服務(wù)和信息安全等;陳楚嬌(1989-)，女，碩士生，研究方向為RFID定位和模型認(rèn)證等。

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