基于有界模型檢驗(yàn)的傳感網(wǎng)軟件驗(yàn)證方法研究.pdf

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

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