本文關鍵詞：面向資源的物聯(lián)網(wǎng)系統(tǒng)形式化建模與驗證　出處：《太原理工大學》2017年碩士論文　論文類型：學位論文

  更多相關文章： 物聯(lián)網(wǎng) 服務化 形式化分析 建模 驗證

【摘要】：隨著物聯(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)轉(zhuǎn)移)架構風格中,任何可被命名的信息都可被抽象為資源。由于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)是一種分布式并發(fā)系統(tǒng),基于物聯(lián)網(wǎng)服務模型可以有效提高形式化分析和驗證的效率,因此,將進程代數(shù)CSP方法應用到物聯(lián)網(wǎng)服務模型的分析和驗證中,有效地確保物聯(lián)網(wǎng)服務的正確性和安全性顯得尤為重要。本文針對以上問題,以物聯(lián)網(wǎng)系統(tǒng)-室內(nèi)空氣質(zhì)量服務為例,采用進程代數(shù)的形式分析方法進行建模與驗證。主要內(nèi)容如下:首先,根據(jù)物聯(lián)網(wǎng)服務的分類,提出室內(nèi)空氣質(zhì)量服務組成框架,并在此基礎上,又提出物聯(lián)網(wǎng)服務按需提供框架;然后,基于面向資源的思想,提出面向資源的物聯(lián)網(wǎng)服務模型,針對標簽遷移系統(tǒng)、并發(fā)系統(tǒng)、實時系統(tǒng)、概率通信順序進程系統(tǒng)、概率實時系統(tǒng)這五種系統(tǒng),對物聯(lián)網(wǎng)服務的行為進行建模與分析,實現(xiàn)了對空氣質(zhì)量服務的快速形式化描述;最后,利用PAT模型檢測器對該物聯(lián)網(wǎng)服務的無死鎖性、無發(fā)散性、確定性、可達性、活性這五種關鍵性質(zhì)進行驗證。通過對特定物聯(lián)網(wǎng)應用場景的建模與驗證,實驗表明在PAT模型檢測器上高效地驗證了該服務的正確性和安全性。
[Abstract]:With the wide application of the Internet of things, complex application scenarios may lead to the wrong operation of the Internet of things system. In order to avoid damage to users, how to use the unified system before the deployment of the system. Efficient modeling and verification is an important problem to be solved. Aiming at the heterogeneity of the Internet of things, it is based on the service-oriented idea. The unified service interface is used to provide the user with the demand, make the Internet of things system service. Describes the functionality of the device in the form of a service. In the REST(Representational State transfer architecture style. Any information that can be named can be abstracted as a resource. Because of the simple form of REST service, the design of rest is more suitable for the resource-limited Internet of things service devices. Based on the resource-oriented core idea of REST, how to model the Internet of things abstractly becomes the most important problem. Secondly, we want to discover the service vulnerabilities before the deployment of the system. It is also necessary to verify and analyze the model. Communication Sequential Processes is the process of communication sequence. CSP is a typical process algebra method to describe the specification and design of distributed concurrent software system, because the Internet of things system is a distributed concurrent system. Based on the Internet of things service model can effectively improve the efficiency of formal analysis and verification, so the process algebra CSP method is applied to the analysis and validation of the Internet of things service model. It is very important to ensure the correctness and security of Internet of things service effectively. In view of the above problems, this paper takes the Internet of things system-Indoor Air quality Service as an example. The main contents are as follows: firstly, according to the classification of Internet of things services, the composition framework of indoor air quality services is proposed, and on this basis. A framework for the on-demand provision of Internet of things services is also proposed; Then, based on the resource-oriented thinking, a resource-oriented Internet of things service model is proposed, aiming at five systems: label migration system, concurrent system, real-time system, probabilistic communication sequence process system and probabilistic real-time system. Modeling and analyzing the behavior of Internet of things (IoT) services, realizing the fast formal description of air quality services; Finally, the PAT model detector is used to solve the problem of deadlock-free, non-divergent, deterministic and reachable. By modeling and validating the specific scenarios of the Internet of things, it is shown that the correctness and security of the service are efficiently verified on the PAT model detector.
【學位授予單位】：太原理工大學
【學位級別】：碩士
【學位授予年份】：2017
【分類號】：TP391.44;TN929.5

【相似文獻】

相關期刊論文 前10條

1 吳雪霽;;把握“物聯(lián)網(wǎng)”時代的三個關鍵點[J];通信世界;2009年33期

2 秦茜;;物聯(lián)網(wǎng)驟成產(chǎn)業(yè)巨浪 各方大肆追捧恐為時尚早[J];IT時代周刊;2009年Z2期

3 石菲;;物聯(lián)網(wǎng)還有多遠[J];中國計算機用戶;2009年Z2期

4 馬繼華;韓文哲;;物聯(lián)網(wǎng)的未來會變成“空中樓閣”嗎?[J];信息網(wǎng)絡;2009年10期

5 ;物聯(lián)網(wǎng)系列報道之一 理性物聯(lián)網(wǎng)[J];通信世界;2009年40期

6 李鵬;;物聯(lián)網(wǎng)發(fā)展 標準與應用先行[J];通信世界;2009年40期

7 李鵬;趙經(jīng)緯;;北郵謝東亮 物聯(lián)網(wǎng)需兩顆紅心一種準備[J];通信世界;2009年40期

8 周雙陽;;尋找物聯(lián)網(wǎng)的制高點[J];通信世界;2009年41期

9 張鵬;;物聯(lián)網(wǎng),十年涅i，

本文編號：1400841