面向資源的物聯(lián)網(wǎng)系統(tǒng)形式化建模與驗(yàn)證.pdf

1、隨著物聯(lián)網(wǎng)系統(tǒng)的廣泛應(yīng)用，復(fù)雜的應(yīng)用場(chǎng)景可能會(huì)導(dǎo)致物聯(lián)網(wǎng)系統(tǒng)錯(cuò)誤運(yùn)行，為了避免給用戶帶來損害，在系統(tǒng)部署之前，如何使用統(tǒng)一、高效的方法進(jìn)行系統(tǒng)地建模、驗(yàn)證成為目前亟待解決的一個(gè)重要問題。針對(duì)物聯(lián)網(wǎng)系統(tǒng)中的異構(gòu)特性，基于面向服務(wù)的思想，用統(tǒng)一的服務(wù)接口為用戶提供需求，使物聯(lián)網(wǎng)系統(tǒng)服務(wù)化，以服務(wù)的形式描述設(shè)備的功能。而在REST(Representational State Transfer，表述性狀態(tài)轉(zhuǎn)移)架構(gòu)風(fēng)格中，任何可被命名的信息都

2、可被抽象為資源。由于REST式服務(wù)形式簡(jiǎn)單、設(shè)計(jì)輕量等特點(diǎn)，REST的設(shè)計(jì)更適合于資源受限的物聯(lián)網(wǎng)服務(wù)設(shè)備。因此，基于REST中面向資源的核心思想，如何對(duì)物聯(lián)網(wǎng)系統(tǒng)進(jìn)行抽象建模成為首要問題。其次，想要在系統(tǒng)部署之前及時(shí)發(fā)現(xiàn)服務(wù)漏洞，還需要對(duì)模型進(jìn)行驗(yàn)證分析。通信順序進(jìn)程(Communication Sequential Processes, CSP)是描述分布式并發(fā)軟件系統(tǒng)規(guī)格和設(shè)計(jì)的一種典型的進(jìn)程代數(shù)方法，由于物聯(lián)網(wǎng)系統(tǒng)是一種分布式并

3、發(fā)系統(tǒng)，基于物聯(lián)網(wǎng)服務(wù)模型可以有效提高形式化分析和驗(yàn)證的效率，因此，將進(jìn)程代數(shù)CSP方法應(yīng)用到物聯(lián)網(wǎng)服務(wù)模型的分析和驗(yàn)證中，有效地確保物聯(lián)網(wǎng)服務(wù)的正確性和安全性顯得尤為重要。
　　本研究以物聯(lián)網(wǎng)系統(tǒng)-室內(nèi)空氣質(zhì)量服務(wù)為例，采用進(jìn)程代數(shù)的形式分析方法進(jìn)行建模與驗(yàn)證。首先，根據(jù)物聯(lián)網(wǎng)服務(wù)的分類，提出室內(nèi)空氣質(zhì)量服務(wù)組成框架，并在此基礎(chǔ)上，又提出物聯(lián)網(wǎng)服務(wù)按需提供框架；然后，基于面向資源的思想，提出面向資源的物聯(lián)網(wǎng)服務(wù)模型，針對(duì)標(biāo)簽遷移