無(wú)線傳感器網(wǎng)絡(luò)（Wireless Sensor Network,簡(jiǎn)稱WSN）的研究起源于軍事領(lǐng)域,隨著人類發(fā)展需要,目前它在軍事、醫(yī)療保健、智能家居、環(huán)境監(jiān)測(cè)、工業(yè)生產(chǎn)和商業(yè)領(lǐng)域都發(fā)揮著其重要的應(yīng)用價(jià)值。就無(wú)線傳感網(wǎng)絡(luò)而言,大多數(shù)情況下需要時(shí)間同步機(jī)制。時(shí)間同步協(xié)議能為網(wǎng)絡(luò)節(jié)點(diǎn)的本地時(shí)間提供共同的時(shí)間戳,為傳感節(jié)點(diǎn)間的感知,通信,能量管理等功能提供前提條件。由于協(xié)議在設(shè)計(jì)過(guò)程中,往往比較復(fù)雜,一點(diǎn)錯(cuò)誤都有可能引起整個(gè)系統(tǒng)故障或者數(shù)據(jù)傳輸錯(cuò)誤。對(duì)協(xié)議的安全性,可靠性以及環(huán)境適用性的分析一直是協(xié)議驗(yàn)證的主要內(nèi)容。模型檢測(cè)是一種適用于協(xié)議性能驗(yàn)證的有效的在形式化方法。本文采用基于時(shí)間自動(dòng)機(jī)的模型檢測(cè)工具Uppaal對(duì)WSN的兩種經(jīng)典的時(shí)間同步協(xié)議（TPSN和FTSP）進(jìn)行模型構(gòu)建。從它們的建模流程中,本文確定了一種用于分析無(wú)線傳感器協(xié)議網(wǎng)絡(luò)的建模方法。即在分析的過(guò)程中把協(xié)議分成主要的幾個(gè)部分,然后再?gòu)牡讓娱_始建模,根據(jù)具體的協(xié)議內(nèi)容對(duì)模型進(jìn)行擴(kuò)展,最后組合成完整的時(shí)間自動(dòng)機(jī)模型。從對(duì)TPSN和FTSP的原理分析中,可以確定TPSN的流程主要分為兩個(gè)階段,分層階段和同步階段。第二個(gè)協(xié)議FTSP... 

【文章來(lái)源】：大連理工大學(xué)遼寧省 211工程院校 985工程院校 教育部直屬院校

【文章頁(yè)數(shù)】：56 頁(yè)

【學(xué)位級(jí)別】：碩士

【文章目錄】：
摘要
Abstract
1 緒論
    1.1 研究背景與意義
    1.2 國(guó)內(nèi)外研究現(xiàn)狀
    1.3 模型檢測(cè)技術(shù)概述
    1.4 本文的章節(jié)安排
2 分析方法和協(xié)議介紹
    2.1 時(shí)間自動(dòng)機(jī)
    2.2 分析方法
    2.3 時(shí)間同步協(xié)議
    2.4 本章小結(jié)
3 時(shí)間同步協(xié)議建模
    3.1 TPSN協(xié)議建模
        3.1.1 TPSN的理想時(shí)間自動(dòng)機(jī)
        3.1.2 TPSN的代價(jià)時(shí)間自動(dòng)機(jī)
    3.2 FTSP協(xié)議建模
        3.2.1 FTSP的理想時(shí)間自動(dòng)機(jī)
        3.2.2 FTSP的代價(jià)時(shí)間自動(dòng)機(jī)
    3.3 本章小結(jié)
4 實(shí)驗(yàn)結(jié)果及性能評(píng)估
    4.1 TPSN性能分析
        4.1.1 正確性驗(yàn)證
        4.1.2 性能對(duì)比
    4.2 FTSP性能分析
        4.2.1 正確性驗(yàn)證
        4.2.2 性能對(duì)比
    4.3 本章小結(jié)
結(jié)論
參考文獻(xiàn)
致謝


【參考文獻(xiàn)】：
期刊論文
[1]螢火蟲模型在水下傳感器網(wǎng)絡(luò)時(shí)間同步中的新應(yīng)用[J]. 金彥亮,方昌立,張曉帥,姚彬.  上海大學(xué)學(xué)報(bào)(自然科學(xué)版). 2017(05)
[2]模型檢測(cè)中狀態(tài)爆炸問(wèn)題研究綜述[J]. 侯剛,周寬久,勇嘉偉,任龍濤,王小龍.  計(jì)算機(jī)科學(xué). 2013(S1)
[3]基于分簇的低功耗多跳無(wú)線傳感器網(wǎng)絡(luò)層次時(shí)間同步算法[J]. 王玉秀,黃劍,石欣,王小剛.  計(jì)算機(jī)應(yīng)用. 2013(02)
[4]基于隨機(jī)時(shí)間自動(dòng)機(jī)和統(tǒng)計(jì)模型檢驗(yàn)技術(shù)的無(wú)線傳感網(wǎng)絡(luò)協(xié)議建模與分析[J]. 張鳳玲,卜磊,王林章,趙建華,李宣東.  中國(guó)科學(xué):信息科學(xué). 2013(01)
[5]無(wú)線傳感器網(wǎng)絡(luò)中一種基于FTSP的時(shí)間同步協(xié)議的改進(jìn)設(shè)計(jì)[J]. 陳瑩,唐加山.  內(nèi)蒙古大學(xué)學(xué)報(bào)(自然科學(xué)版). 2012(04)
[6]無(wú)線傳感器網(wǎng)絡(luò)應(yīng)用系統(tǒng)最新進(jìn)展綜述[J]. 洪鋒,褚紅偉,金宗科,單體江,郭忠文.  計(jì)算機(jī)研究與發(fā)展. 2010(S2)
[7]無(wú)線傳感器網(wǎng)絡(luò)的時(shí)間同步技術(shù)[J]. 謝潔銳,胡月明,劉才興,劉蘭.  計(jì)算機(jī)工程與設(shè)計(jì). 2007(01)
[8]無(wú)線傳感器網(wǎng)絡(luò)[J]. 任豐原,黃海寧,林闖.  軟件學(xué)報(bào). 2003(07)

碩士論文
[1]基于統(tǒng)計(jì)模型檢測(cè)的無(wú)線傳感器網(wǎng)絡(luò)協(xié)議建模與分析[D]. 楊樹峰.鄭州大學(xué) 2015
[2]SPIN模型檢測(cè)的形式化分析機(jī)理研究及應(yīng)用[D]. 劉俏威.南昌大學(xué) 2008



本文編號(hào)：3108339