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

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

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

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