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

有效

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

1.?一種基于模型檢測的無線傳感器網絡時間同步檢驗方法，其特征在于該檢驗方法包括模型生成優(yōu)化器、能量感知模塊、時間可達性規(guī)范模塊、時間同步模型檢測器和結果生成模塊，所述的時間可達性規(guī)范模塊連接能量感知模塊、時間同步模型檢測器和待檢測的時間同步機制，所述的模型生成優(yōu)化器連接時間同步模型檢測器，時間同步模型檢測器通向結果生成模塊，所述方法包含的步驟為：

（1）建立時間可達性規(guī)范

可達性規(guī)范的建立依據(jù)兩個方面的內容：待檢測時間同步機制和能量；

1）輸入待檢測時間同步機制

本發(fā)明所述時間可達性規(guī)范利用網絡的跳數(shù)來計算需要節(jié)點間時間同步的區(qū)域范圍，根據(jù)同步范圍來確定最大時間同步誤差MAX_SYNC，最大時間同步誤差將隨著同步范圍的增大而增加；

2）感知能量

本發(fā)明所述的能量感知模塊將能量分布消息傳遞給時間可達性規(guī)范模塊，必需的網絡通信和計算負載是可預知的，在建立時間可達性規(guī)范時均勻使用網絡節(jié)點的能量來達到能量的高效使用；

具體描述方法是：把希望系統(tǒng)將要滿足的屬性結合待檢測時間同步機制和能量感知模塊用時序邏輯進行表達；

時序邏輯是模型檢測的基礎，對一個系統(tǒng)進行

模型檢測，需要用時序邏輯公式來描述期望的性質；

（2）生成優(yōu)化模型

優(yōu)化模型的生成使用模型生成優(yōu)化器，具體包括模型生成和模型的優(yōu)化；

1）生成初步模型

對被檢測的時間同步機制進行建模，將被檢驗的機制轉化為一種形式化的狀態(tài)自動機模型，以便于后面檢驗其是否滿足給定規(guī)范；使用標有時間標記的狀態(tài)圖進行建模，即轉換系統(tǒng)，轉換系統(tǒng)是一個四元組（∑，S，S0，E)；

2）生成優(yōu)化模型

優(yōu)化狀態(tài)自動機模型，狀態(tài)自動機減少自動機中的對驗證過程不產生影響的狀態(tài)；首先將狀態(tài)自動機進行遍歷，刪除狀態(tài)自動機中不屬于通道的所有事件對上的消息，對產生的狀態(tài)自動機的狀態(tài)進行遍歷，如果一個狀態(tài)上沒有時鐘解釋，

其前驅遷移或者后繼遷移都為空，刪除此狀態(tài)，對與此狀態(tài)有關的遷移進行合并；

（3）檢測時間同步機制

本發(fā)明所述的模型檢測器完成模型檢測的功能，模型檢測器將與應用相關的時間可達性規(guī)范和模型生成優(yōu)化器優(yōu)化后的待檢測時間同步機制模型作為輸入，而由模型檢測器自動檢測建立的模型是否符合時間可達性規(guī)范；

輸出是正確或反例，若模型符合時間可達性規(guī)范，證明機制是正確的，反之，輸出反例，根據(jù)反例來判斷產生反例的原因；

（4）輸出結果

將模型檢測器的結果輸出到結果生成器中進行處理，若時間同步機制不正確，輸出反例，并經過結果生成器生成測試人員易懂的語言。

2.根據(jù)權利要求1所述的一種基于模型檢測的無線傳感器網絡時間同步檢驗方法，其特征在于所述的基于模型檢測的無線傳感器網絡時間同步檢驗方法包括模型生成優(yōu)化器、能量感知模塊、時間可達性規(guī)范模塊、時間同步模型檢測器和結果生成模塊。

3.根據(jù)權利要求2所述的一種基于模型檢測的無線傳感器網絡時間同步檢驗方法，其特征在于所述的模型生成優(yōu)化器將被檢測的時間同步機制轉化為一種形式化的狀態(tài)自動機模型，并對已建立模型進行優(yōu)化，減少自動機中的對驗證過程不產生影響的狀態(tài)。

4.根據(jù)權利要求2所述的一種基于模型檢測的無線傳感器網絡時間同步檢驗方法，其特征在于所述的能量感知模塊將能量分布消息傳遞給時間可達性規(guī)范模塊，在建立時間可達性規(guī)范時將能量消耗和剩余能量考慮進去。

5.根據(jù)權利要求2所述的一種基于模型檢測的無線傳感器網絡時間同步檢驗方法，其特征在于所述的時間可達性規(guī)范模塊把希望系統(tǒng)將要滿足的屬性結合待檢測時間同步機制和能量感知模塊用時序邏輯進行表達。

6.根據(jù)權利要求2所述的一種基于模型檢測的無線傳感器網絡時間同步檢驗方法，其特征在于模型檢測檢測器將所述的已優(yōu)化的時間同步模型與所述的時間可達性規(guī)范進行對比檢驗，判斷所述被檢測機制是否違背可達性規(guī)范。

7.根據(jù)權利要求2所述的一種基于模型檢測的無線傳感器網絡時間同步檢驗方法，其特征在于所述結果生成模塊將模型檢測器的輸出轉化為檢測人員易懂的形式。