[發明專利]一種基于模型檢測的無線傳感器網絡時間同步檢驗方法

有效

• 申請號: 201210006008.X
• 申請日: 2012-01-10
• 公開（公告）號: CN102624476A
• 公開（公告）日: 2012-08-01
• 發明（設計）人: 陳志;彭婭;岳文靜
• 申請（專利權）人: 南京郵電大學
• 主分類號: H04J3/06
• 分類號: H04J3/06;H04L29/08
• 代理公司: 南京經緯專利商標代理有限公司 32200
• 代理人: 葉連生

技術領域

本發明涉及一種在傳感器網絡中時間同步檢測的方法，主要利用模型檢測技術來解決傳感器網絡時間同步的問題，屬于計算機技術、無線通信、傳感器技術、實時技術、分布式系統和驗證技術交叉技術應用領域。

背景技術

傳感器技術、微機電系統、現代網絡和無線通信等技術的進步，推動了現代無線傳感器網絡的產生和發展。無線傳感器網絡擴展了人們信息獲取能力，將客觀世界的物理信息同傳輸網絡連接在一起，在下一代網絡中將為人們提供最直接、最有效、最真實的信息。無線傳感器網絡是由一組傳感器以Ad?Hoc方式構成的無線網絡，其目的是協作地感知、采集和處理網絡覆蓋地理區域中感知對象的信息，并發布給觀察者。從上述定義可以看到，傳感器、感知對象和觀察者是無線傳感器網絡的3個基本要素；無線是傳感器之間、傳感器與觀察者之間的通信方式，用于在傳感器與觀察者之間建立通信路徑：協作地感知、采集、處理、發布感知信息是無線傳感器網絡的基本功能；一組功能有限的傳感器協作地完成大的感知任務是無線傳感器網絡的重要特點。無線傳感器網絡可以被廣泛地應用于軍事應用、醫療護理、環境監測、空間探索、醫療衛生、制造業和反恐抗災等帶有明顯應用需求的領域。

時間同步是需要協同工作的傳感器網絡系統的一個關鍵機制，無論是設計還是應用中時間同步都是非常重要的。時間同步的目的就是對各個節點的本地時鐘提供一個統一的時間標尺。在無線傳感器網絡中，各節點都有自己的時鐘，在需要事件的時間的時候，就要求這些節點的時鐘必須一致。在無線傳感器網絡的許多應用中，用戶向無線傳感器網絡咨詢或無線傳感器網絡向外部網絡報告都需要說明事件發生的時間。當無線傳感器網絡用于目標識別和追蹤時，許多傳感器節點只觀測目標對象的單一物理現象，并不能得到目標的類別、位置、速度或前進方向等信息，要想得到所需要的詳細信息，就必須進行在網計算——多個節點感應的信息進行信息協同處理或數據融合。這就要求相關的傳感器節點所采集的數據在時間上是關聯的，有時甚至要求是同步的。不同的無線傳感器網絡和不同的應用對時間同步的要求是不一樣的。從精度上來說，時間同步的要求相當嚴格，經常要求在像目標跟蹤這樣的任務中，能達到微秒級的精度；而在有的應用中只需要達到毫秒級。這些諸如此類的因素，使得無線傳感器網絡中時間同步的研究相對于其他的分布式網絡中的時間同步來說要復雜得多。

模型檢測方法可以在構建系統前對系統的安全性和可靠性進行驗證，以盡早發現錯誤。模型檢測(ModelChecking)是對有窮狀態系統的一種形式化確認方法。它最早由Clarke和Emerson以及Quielle和Sifakis在1981年分別提出的，主要通過顯式狀態搜索或隱式不動點計算來驗證有窮狀態并發系統的模態/命題性質。實質是利用計算機的快速計算能力，通過窮舉被檢驗系統的狀態空間中的每一個狀態來驗證該系統滿足特定的形式描述。盡管限制在有窮系統上是一個缺點，但模型檢測可以應用于許多非常重要的系統，如通信協議和電路的驗證上。很多情況下，可以把模型檢測和各種抽象與歸納原則結合起來驗證非有窮狀態系統(如實時系統)，模型檢測的基本思想是用狀態遷移系統(S)表示系統的行為，用模態/時序邏輯公式(F)描述系統的性質，這樣“系統是否滿足所期望的性質”就轉化為數學問題“狀態遷移系統S是否公式F的一個模型”，用公式表示為S|＝F？。對有窮狀態系統，這個問題是可判定的，即可以用計算機程序在有限時間內自動確定。模型檢測已被應用于計算機硬件、通信協議、控制系統、安全認證協議等方面的分析與驗證中，取得了令人矚目的成功，并從學術界輻射到了產業界。

模型檢測其基本原理實現為系統建立形式化模型，闡述所要驗證的性質，然后用算法去檢測該模型是否滿足所述性質。模型檢測提供一個完整的系統屬性驗證框架，模型檢測的優點是模型檢驗能達到完全自動化的程度，只需用有窮狀態模型和邏輯公式分別將系統實現和待驗證的系統規范描述出來，之后的判斷過程則完全可以由模型檢測工具自動完成，不需要人的參與；模型檢驗過程總會以“是”或“否”的結果中止，當以“否”的結果中止時，說明設計或系統不滿足某個給定的性質。此時一個違反性質的行為反例將會被給出，此反例將對理解錯誤的真正原因和修正錯誤提供線索。由于模型檢測技術有以上優點，利用它對無線傳感器網絡進行同步機制的檢驗，在其設計階段盡可能的找出錯誤。

發明內容

技術問題：本發明的目的是提供一種基于模型檢測的無線傳感器網絡時間同步檢驗方法，該同步檢驗方法分析能力強、可讀性高，從而滿足分析與應用相關的同步機制的要求，達到快速發現同步的不可靠和不安全性，提高和改進時間同步機制。