物聯(lián)網(wǎng)服務(wù)的建模和驗(yàn)證是物聯(lián)網(wǎng)研究中的重要問題。文中對混成自動(dòng)機(jī)進(jìn)行了擴(kuò)展,提出了具有位置驅(qū)動(dòng)特點(diǎn)的時(shí)空I/O混成自動(dòng)機(jī)。文中提出了基于時(shí)空I/O混成自動(dòng)機(jī)的物聯(lián)網(wǎng)服務(wù)建模與驗(yàn)證框架。在框架中,首先對物聯(lián)網(wǎng)服務(wù)進(jìn)行了描述,并使用時(shí)空I/O混成自動(dòng)機(jī)對物聯(lián)網(wǎng)服務(wù)進(jìn)行建模。這些時(shí)空I/O混成自動(dòng)機(jī)形成一個(gè)網(wǎng)絡(luò),刻畫完整的物聯(lián)網(wǎng)服務(wù)的通信并行過程。文中采用的形式化驗(yàn)證方法為微分動(dòng)態(tài)邏輯(Differential Dynamic Logic,DL),其操作模型為HP(Hybrid Program)。利用DL可以將所建模型轉(zhuǎn)換為對應(yīng)的HP。結(jié)合得到的HP對驗(yàn)證的物聯(lián)網(wǎng)服務(wù)性質(zhì)進(jìn)行規(guī)約,最后使用定理證明器KeYmaera驗(yàn)證物聯(lián)網(wǎng)服務(wù)的正確性。

【文章頁數(shù)】：7 頁

【文章目錄】：
0 引言
1 基于時(shí)空I/O混成自動(dòng)機(jī)的物聯(lián)網(wǎng)服務(wù)建模與驗(yàn)證的框架
    1.1 一個(gè)物聯(lián)網(wǎng)典型應(yīng)用場景
    1.2 物聯(lián)網(wǎng)服務(wù)
    1.3 時(shí)空I/O混成自動(dòng)機(jī)
        1.3.1混成自動(dòng)機(jī)
        1.3.2 時(shí)空I/O混成自動(dòng)機(jī)的定義
    1.4 物聯(lián)網(wǎng)實(shí)體和服務(wù)模型
    1.5 基于時(shí)空I/O混成自動(dòng)機(jī)的物聯(lián)網(wǎng)服務(wù)建模與驗(yàn)證框架
2 基于時(shí)空I/O混成自動(dòng)機(jī)的物聯(lián)網(wǎng)服務(wù)建模
    2.1 描述物聯(lián)網(wǎng)服務(wù)
    2.2 基于時(shí)空I/O混成自動(dòng)機(jī)的物聯(lián)網(wǎng)服務(wù)模型
    2.3基于時(shí)空I/O混成自動(dòng)機(jī)的物聯(lián)網(wǎng)服務(wù)建模
3 微分動(dòng)態(tài)邏輯驗(yàn)證方法與Hybrid Program
    3.1 微分動(dòng)態(tài)邏輯
    3.2 微分動(dòng)態(tài)邏輯模型
4 案例驗(yàn)證
    4.1 模型的驗(yàn)證
    4.2 驗(yàn)證和分析
5 結(jié)束語



本文編號：3778961