隨著新一代網(wǎng)絡(luò)技術(shù)和硬件設(shè)備的實現(xiàn),物聯(lián)網(wǎng)(Internet of Things)技術(shù)得到了空前地研究和發(fā)展,其應(yīng)用也逐步進入市場化階段,從智慧城市,野外考察工作站,到微型心率控制系統(tǒng)等。地球上的任何一個物體都可以成為物聯(lián)網(wǎng)的組成部分,因此物聯(lián)網(wǎng)的規(guī)模將會相當龐大,其實現(xiàn)難度以及交互機制的復(fù)雜性也會急劇增加。在設(shè)計層保證物聯(lián)網(wǎng)應(yīng)用的正確性成為關(guān)鍵和難點。本文從軟件工程角度出發(fā),根據(jù)“高內(nèi)聚低耦合”的設(shè)計原則,將物聯(lián)網(wǎng)各個組成單元抽象為具有接口的獨立組件,側(cè)重于組件之間通信交互的正確性、合理性,研究由此形成的物聯(lián)網(wǎng)交互系統(tǒng)。人們通常從測試的角度研究一個系統(tǒng)的可執(zhí)行性,但這樣并不能保證該系統(tǒng)的正確性。本文使用形式化方法,針對物聯(lián)網(wǎng)交互系統(tǒng)具有的特征進行建模,并從概率、時間、代價、數(shù)據(jù)流等非功能性需求方面對系統(tǒng)應(yīng)滿足的性質(zhì)進行量化驗證分析,從而保證系統(tǒng)運行的正確性。以此提供了一種對物聯(lián)網(wǎng)交互系統(tǒng)進行分析驗證的形式化方法。本文主要工作和創(chuàng)新點有以下四個方面:1.建立了物聯(lián)網(wǎng)交互系統(tǒng)的形式化描述模型。針對物聯(lián)網(wǎng)交互系統(tǒng)靈活多變的網(wǎng)絡(luò)拓撲結(jié)構(gòu),以及以通信交互為主的特性,本文在Reo通信模型基礎(chǔ)上擴展概率、時間、代價等方面的表達能力,提出物聯(lián)網(wǎng)交互系統(tǒng)的形式化描述模型——Reo。進一步給出該模型的語義模型——pPTCA。人們可以很方便地通過描述模型對物聯(lián)網(wǎng)交互系統(tǒng)進行建模,同時利用對應(yīng)的語義模型進行相關(guān)的形式化驗證分析。2.構(gòu)建了物聯(lián)網(wǎng)交互系統(tǒng)性質(zhì)的邏輯表達系統(tǒng)。為了規(guī)范代價約束、概率性、時間性等物聯(lián)網(wǎng)交互系統(tǒng)的特征,本文選取作為基礎(chǔ)邏輯�？紤]到物聯(lián)網(wǎng)交互系統(tǒng)中資源的重要性以及通信交互的數(shù)據(jù)驅(qū)動性,在該邏輯上分別擴展數(shù)據(jù)流及代價行為的表達能力,構(gòu)建了物聯(lián)網(wǎng)交互系統(tǒng)性質(zhì)的刻畫邏輯——pPTDL。為了集成Modest工具進行自動化驗證,本文研究了從pPTCA的反應(yīng)式模型到支持動作集的隨機時間自動機的轉(zhuǎn)換機制,為該工具的使用提供了理論支撐。3.研究了物聯(lián)網(wǎng)交互系統(tǒng)模型的互模擬等價。物聯(lián)網(wǎng)交互系統(tǒng)規(guī)模的龐大必然導(dǎo)致形式化模型的復(fù)雜,這將給量化驗證分析帶來極大的困難。為了合理約減模型的規(guī)模,本文從是否考慮系統(tǒng)內(nèi)部行為的角度,分別對強互模擬以及弱互模擬進行研究。針對強互模擬,本文研究具有概率、時間、代價等特征的約束自動機模型的行為等價。針對弱互模擬,本文側(cè)重于概率模型,并考慮到發(fā)散行為(即無限內(nèi)部行為)所帶來的重要影響,從三個角度研究了保發(fā)散弱概率互模擬的相關(guān)理論以及對應(yīng)的驗證方法。通過結(jié)合歸納思想以及經(jīng)典剖分精化方法,本文設(shè)計了計算最大保發(fā)散弱概率互模擬的多項式時間算法。4.介紹了偏遠環(huán)境下獨立工作的小型野外工作站物聯(lián)網(wǎng)交互系統(tǒng)案例。通過應(yīng)用本文提出的模型與邏輯,對該物聯(lián)網(wǎng)交互系統(tǒng)進行建模并對其具有的性質(zhì)進行邏輯規(guī)范,在此基礎(chǔ)上完成量化驗證與分析,從而表明了本文提出物聯(lián)網(wǎng)交互系統(tǒng)量化驗證方法的有效性。
【學(xué)位單位】：華東師范大學(xué)
【學(xué)位級別】：博士
【學(xué)位年份】：2019
【中圖分類】：TP391.44;TN929.5
【文章目錄】：
摘要
abstract
主要命名中英對照表
主要標號說明
主要符號索引
第一章 緒論
    1.1 研究背景與動機
    1.2 研究現(xiàn)狀與相關(guān)工作
    1.3 本文工作與主要創(chuàng)新點
    1.4 組織結(jié)構(gòu)
    1.5 本章小結(jié)
第二章 預(yù)備知識
    2.1 數(shù)學(xué)符號
    2.2 概率理論
    2.3 形式化模型Reo
    2.4 約束自動機理論
    2.5 時態(tài)邏輯
    2.6 本章小結(jié)
第三章 物聯(lián)網(wǎng)交互系統(tǒng)模型
    3.1 引言
    3.2 代價概率時間Reo模型
    3.3 代價概率時間約束自動機
    3.4 代價概率時間約束自動機語義
        3.4.1 概率時間系統(tǒng)
        3.4.2 自動機語義
    3.5 本章小結(jié)
第四章 物聯(lián)網(wǎng)交互系統(tǒng)性質(zhì)規(guī)范
    4.1 代價概率時間數(shù)據(jù)流邏輯
    4.2 代價概率時間數(shù)據(jù)流邏輯解釋
        4.2.1 邏輯解釋
        4.2.2 模型性質(zhì)可滿足性
        4.2.3 邏輯表達能力分析
        4.2.4 一體化還是組合化的邏輯依據(jù)
    4.3 工具自動化驗證
        4.3.1 pPTCA的簡化模型
        4.3.2 支持動作集的STA模型
        4.3.3 spPTCA到MSTA的轉(zhuǎn)換
    4.4 本章小結(jié)
第五章 模型行為等價研究
    5.1 強互摸擬研究
        5.1.1 經(jīng)典強互模擬
        5.1.2 代價約束的強互摸擬
        5.1.3 代價約束的強概率互模擬
    5.2 弱互摸擬研究
        5.2.1 概率模型
        5.2.2 經(jīng)典弱概率互模擬
        5.2.3 定性保發(fā)散弱互摸擬
        5.2.4 定性保等價發(fā)散弱互模擬
        5.2.5 定量保發(fā)散弱互模擬
        5.2.6 概率系統(tǒng)與非概率系統(tǒng)一致性
    5.3 最大保發(fā)散弱互模擬的計算算法
        5.3.1 定性保等價發(fā)散弱互模擬的判定算法
        5.3.2 最大定性保等價發(fā)散弱互模擬的計算算法
    5.4 本章小結(jié)
第六章 應(yīng)用案例分析
    6.1 野外工作站物聯(lián)網(wǎng)交互系統(tǒng)建模
        6.1.1 物理場景需求分析
        6.1.2 物聯(lián)網(wǎng)交互系統(tǒng)建模
    6.2 野外工作站物聯(lián)網(wǎng)交互系統(tǒng)性質(zhì)分析
        6.2.1 升級前的系統(tǒng)
        6.2.2 升級后的系統(tǒng)
    6.3 本章小結(jié)
第七章 總結(jié)與展望
    7.1 本文工作總結(jié)
    7.2 后續(xù)工作展望
參考文獻
致謝
發(fā)表論文和科研情況

【參考文獻】

相關(guān)期刊論文 前2條

1 劉小洋;伍民友;;車聯(lián)網(wǎng):物聯(lián)網(wǎng)在城市交通網(wǎng)絡(luò)中的應(yīng)用[J];計算機應(yīng)用;2012年04期

2 朱洪波;楊龍祥;于全;;物聯(lián)網(wǎng)的技術(shù)思想與應(yīng)用策略研究[J];通信學(xué)報;2010年11期

本文編號：2827514