基于有界模型檢驗的傳感網軟件驗證方法研究.pdf

1、傳感網是一種由具有感知、處理和無線通信能力的傳感器節(jié)點通過自組織方式形成的一種多跳網絡。隨著傳感網的迅速發(fā)展，傳感網軟件的規(guī)模逐漸變大，這使得不同的應用領域對傳感網軟件的性能都有著越來越高的要求。軟件驗證技術是保證軟件性能的一項重要技術。模型檢驗是軟件驗證技術的一種，它為傳感網軟件驗證提供了新的技術手段。在基于模型檢驗的軟件驗證領域中，狀態(tài)空間爆炸問題是其發(fā)展的瓶頸。有界模型檢驗技術是模型檢驗領域新的研究方向，它通過限制建立模型時狀態(tài)展

2、開的次數來實現，主要用于緩解狀態(tài)空間爆炸問題。
　　本文主要對基于有界模型檢驗的傳感網軟件驗證方法進行研究，該研究是面向源代碼的，其實現主要分為兩個工作：
　　1）提出一種基于有界模型檢驗的傳感網軟件代碼驗證方法。該方法首先通過對傳感網軟件建立軟件模型，實現對傳感網軟件的靜態(tài)結構和動態(tài)行為的抽象；然后定義模型轉換規(guī)則，將軟件模型轉化C語言代碼；最后使用CBMC對轉化后的代碼進行有界模型檢驗。
　　2）提出一種基于POR