基于時(shí)態(tài)描述邏輯的語(yǔ)義物聯(lián)網(wǎng)服務(wù)驗(yàn)證

1、 密 級(jí) 碩 士 學(xué) 位 論 文 題目 基于時(shí)態(tài)描述邏輯的語(yǔ)義物聯(lián)網(wǎng)服務(wù)驗(yàn)證 （英文） （英文）Verification of SWOT Services Based on Temporal Logic 研 究 生 學(xué) 號(hào): 1403201021 研 究 生 姓 名: 韓 喬 指導(dǎo)教師姓名、職

2、稱 指導(dǎo)教師姓名、職稱: 常 亮（教授） 申 請(qǐng) 學(xué) 位 門(mén) 類(lèi): 工學(xué)碩士 學(xué) 科、專(zhuān) 科、專(zhuān) 業(yè): 計(jì)算機(jī)科學(xué)與技術(shù) 論 文 答 辯 日 期: 2017 年 6 月 8 日 摘要 I 摘 要 隨著信息時(shí)代的來(lái)臨， 物聯(lián)網(wǎng)早已成為信息化發(fā)展中不可或缺的一部分。 為了使物聯(lián)網(wǎng)更加智能化，將語(yǔ)義引入物聯(lián)網(wǎng)中，形成

3、語(yǔ)義物聯(lián)網(wǎng)。將語(yǔ)義物聯(lián)網(wǎng)與面向服務(wù)的方法相結(jié)合， 可以高效的利用物聯(lián)網(wǎng)中的信息資源。 而語(yǔ)義物聯(lián)網(wǎng)服務(wù)的正確與否卻是一個(gè)有待驗(yàn)證的問(wèn)題。 針對(duì)語(yǔ)義物聯(lián)網(wǎng)服務(wù)的正確性驗(yàn)證問(wèn)題， 文中采用描述邏輯與傳統(tǒng)時(shí)態(tài)邏輯相結(jié)合的方式。 使用描述邏輯對(duì)系統(tǒng)建模中的領(lǐng)域知識(shí)進(jìn)行刻畫(huà)， 同時(shí)引入領(lǐng)域知識(shí)推理機(jī)制，將其與傳統(tǒng)的模型檢測(cè)機(jī)制相融合。 本文首先在領(lǐng)域知識(shí)的驅(qū)動(dòng)下， 利用帶有 ABox 標(biāo)注的狀態(tài)遷移系統(tǒng)對(duì)語(yǔ)義物聯(lián)網(wǎng)服務(wù)進(jìn)行建模，其次將描述邏輯 A

4、LC 分別與命題 μ-演算和概率計(jì)算樹(shù)邏輯相結(jié)合對(duì)待驗(yàn)證性質(zhì)進(jìn)行刻畫(huà)，并給出具體的模型檢測(cè)算法。 研究工作如下： （1）給出了一種基于時(shí)態(tài)描述邏輯 ALC-μ 的建模和驗(yàn)證方法。時(shí)態(tài)描述邏輯ALC-μ 是將描述邏輯的刻畫(huà)能力與命題 μ-演算的表示能力相結(jié)合后的一種邏輯系統(tǒng)。在命題 μ-演算的基礎(chǔ)上構(gòu)建了時(shí)態(tài)描述邏輯 ALC-μ，一方面使用 μ-演算的時(shí)態(tài)算子表示系統(tǒng)的性質(zhì)， 另一方面使用描述邏輯對(duì)領(lǐng)域知識(shí)進(jìn)行刻畫(huà)。 并針對(duì)上述所構(gòu)建的邏

5、輯系統(tǒng)，提出時(shí)態(tài)描述邏輯 ALC-μ 的模型檢測(cè)算法。與命題 μ-演算相比較，該模型檢測(cè)算法將描述邏輯 ALC 的推理機(jī)制與模型檢測(cè)機(jī)制相融合，可以用來(lái)對(duì)語(yǔ)義物聯(lián)網(wǎng)服務(wù)的正確性進(jìn)行驗(yàn)證。并且為了更好的將理論應(yīng)用于實(shí)際，在 ALC-μ 的模型檢測(cè)算法的基礎(chǔ)上開(kāi)發(fā)出相應(yīng)的驗(yàn)證軟件。 （2）給出了一種基于概率時(shí)態(tài)描述邏輯 ALC-PCTL 的建模和驗(yàn)證方法。首先，利用描述邏輯中的 ABox 對(duì)概率自動(dòng)機(jī)進(jìn)行標(biāo)注， 引入語(yǔ)義標(biāo)注的概率有限自動(dòng)機(jī)