金仙力，陳楚嬌

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

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

金仙力，陳楚嬌

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

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

RFID定位系統(tǒng);時(shí)間自動(dòng)機(jī);UPPAAL;模型驗(yàn)證

1 概述

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

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

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

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

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

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

2 相關(guān)理論

2.1 時(shí)間自動(dòng)機(jī)理論

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

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

定義2(時(shí)間自動(dòng)機(jī)的語(yǔ)義):設(shè)(L，l0，C，A，E，I)是一個(gè)時(shí)間自動(dòng)機(jī)，其語(yǔ)義可表示為一個(gè)標(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＇)，對(duì)于d∈R≥0，u+d把C中的每個(gè)時(shí)鐘x映射為u(x)+d，［r|→0］u表示時(shí)鐘值，其中r中的時(shí)鐘被復(fù)位為0，C中其他時(shí)鐘仍保持為u。

定義3(時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)的語(yǔ)義):設(shè)Ai=(Li，l0i，C，A，Ei，Ii)是時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)，=(l01，l02，…，l0n)是初始位置向量。Ai的語(yǔ)句可表示為標(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 自動(dòng)驗(yàn)證工具UPPAAL

UPPAAL是由丹麥的Aalborg大學(xué)和瑞士的Uppsala大學(xué)于1995年聯(lián)合開(kāi)發(fā)，具有世界先進(jìn)水平的實(shí)時(shí)系統(tǒng)模擬和驗(yàn)證工具［10］。它可以描述成非確定并行過(guò)程的系統(tǒng)。每個(gè)過(guò)程被描述為由有限控制結(jié)構(gòu)、實(shí)數(shù)值時(shí)鐘及變量組成的時(shí)間自動(dòng)機(jī)。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(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)證請(qǐng)求消息后，轉(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消息后，驗(yàn)證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請(qǐng)求認(rèn)證消息后，轉(zhuǎn)至狀態(tài)rCheckId，之后收到tag發(fā)來(lái)的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ā)來(lái)的keyid1消息，則轉(zhuǎn)至狀態(tài)rMatchKey-Id1，然后向tag發(fā)送dkey消息，轉(zhuǎn)至狀態(tài)rIsMatchKey，此時(shí)若收到tag發(fā)來(lái)的nomatch2消息，那么向processor發(fā)送nomatchdkey消息，轉(zhuǎn)至初始狀態(tài)rStart，若收到的是tag發(fā)來(lái)的tid消息時(shí)，則要看tag發(fā)來(lái)的ID與processor發(fā)來(lái)的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ā)來(lái)的tmetaid1消息后，轉(zhuǎn)至狀態(tài)pCheckId，之后向database發(fā)送matchid消息，轉(zhuǎn)至狀態(tài)pIsMatchId，若收到database發(fā)來(lái)的nomatchid消息，則轉(zhuǎn)至狀態(tài)pNotMatchId，然后向processor發(fā)送 fail的消息，并回到初始狀態(tài)pStart;若收到的是database發(fā)來(lái)的keyid消息，轉(zhuǎn)至狀態(tài)pMatchKeyId，并向reader發(fā)送keyid1消息，轉(zhuǎn)至狀態(tài)pIsMatchKeyId，如果收到 reader發(fā)來(lái)的nomatchtid消息，那么回到初始狀態(tài)pStart，如果收到reader發(fā)來(lái)的nomatchdkey消息，也回到初始狀態(tài)pStart，如果收到reader發(fā)來(lái)的rid消息，則轉(zhuǎn)至狀態(tài)pMatchId，然后向database發(fā)送search消息，轉(zhuǎn)至狀態(tài)pSearch，此時(shí)若收到database發(fā)來(lái)的come消息，則轉(zhuǎn)至狀態(tài)pComeIn，并向database發(fā)送 updatelocation消息，回到初始狀態(tài)pStart，若收到database發(fā)來(lái)的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ā)來(lái)的matchid消息，轉(zhuǎn)至狀態(tài)dCheckId，并查詢自己的數(shù)據(jù)庫(kù)是否存在與metaID匹配的項(xiàng)，若找到，轉(zhuǎn)至狀態(tài)dMatchId，之后向processor發(fā)送keyid消息，回到初始狀態(tài)dStart;若未找到，轉(zhuǎn)至狀態(tài)dNotMatchId，之后向processor發(fā)送nomatchid消息，并回到初始狀態(tài)dStart。如果ID卡驗(yàn)證成功，則會(huì)收到processor發(fā)來(lái)的search消息，轉(zhuǎn)至狀態(tài)dSearchregion，若是外閱讀器，則轉(zhuǎn)至狀態(tài)dLeave，并向processor發(fā)送leave消息，轉(zhuǎn)至狀態(tài)dLeaveMid，之后收到processor發(fā)來(lái)的null消息，回到初始狀態(tài)dStart;若是內(nèi)讀寫(xiě)器，則轉(zhuǎn)至狀態(tài)dCome，并向processor發(fā)送come消息，轉(zhuǎn)至狀態(tài)dComeMid，之后收到processor發(fā)來(lái)的updatelocation消息，回到初始狀態(tài)dStart。具體的數(shù)據(jù)庫(kù)進(jìn)程模板如4所示。

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

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

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

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

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

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

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

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

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

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

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

4.3 驗(yàn)證結(jié)果

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

5 結(jié)束語(yǔ)

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

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

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

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

［4］ 杜治國(guó)，楊 波，歐陽(yáng)國(guó)幀，等.安全的RFID認(rèn)證協(xié)議研究設(shè)計(jì)［J］.計(jì)算機(jī)工程和設(shè)計(jì)，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é)議的自動(dòng)驗(yàn)證［J］.河南師范大學(xué)學(xué)報(bào):自然科學(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ò)出版時(shí)間:

時(shí)間:2016-08-01

國(guó)家自然科學(xué)基金資助項(xiàng)目(61373139)

金仙力(1978-)，男，博士，副教授，研究方向?yàn)樾问交椒āeb服務(wù)和信息安全等;陳楚嬌(1989-)，女，碩士生，研究方向?yàn)镽FID定位和模型認(rèn)證等。

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