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

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

【摘要】：隨著物聯(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)行,為了避免給用戶帶來(lái)?yè)p害,在系統(tǒng)部署之前,如何使用統(tǒng)一、高效的方法進(jìn)行系統(tǒng)地建模、驗(yàn)證成為目前亟待解決的一個(gè)重要問(wèn)題。針對(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)格中,任何可被命名的信息都可被抽象為資源。由于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)行抽象建模成為首要問(wè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)是一種分布式并發(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ù)的正確性和安全性顯得尤為重要。本文針對(duì)以上問(wèn)題,以物聯(lián)網(wǎng)系統(tǒng)-室內(nèi)空氣質(zhì)量服務(wù)為例,采用進(jìn)程代數(shù)的形式分析方法進(jìn)行建模與驗(yàn)證。主要內(nèi)容如下:首先,根據(jù)物聯(lián)網(wǎng)服務(wù)的分類,提出室內(nèi)空氣質(zhì)量服務(wù)組成框架,并在此基礎(chǔ)上,又提出物聯(lián)網(wǎng)服務(wù)按需提供框架;然后,基于面向資源的思想,提出面向資源的物聯(lián)網(wǎng)服務(wù)模型,針對(duì)標(biāo)簽遷移系統(tǒng)、并發(fā)系統(tǒng)、實(shí)時(shí)系統(tǒng)、概率通信順序進(jìn)程系統(tǒng)、概率實(shí)時(shí)系統(tǒng)這五種系統(tǒng),對(duì)物聯(lián)網(wǎng)服務(wù)的行為進(jìn)行建模與分析,實(shí)現(xiàn)了對(duì)空氣質(zhì)量服務(wù)的快速形式化描述;最后,利用PAT模型檢測(cè)器對(duì)該物聯(lián)網(wǎng)服務(wù)的無(wú)死鎖性、無(wú)發(fā)散性、確定性、可達(dá)性、活性這五種關(guān)鍵性質(zhì)進(jìn)行驗(yàn)證。通過(guò)對(duì)特定物聯(lián)網(wǎng)應(yīng)用場(chǎng)景的建模與驗(yàn)證,實(shí)驗(yàn)表明在PAT模型檢測(cè)器上高效地驗(yàn)證了該服務(wù)的正確性和安全性。
[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.
【學(xué)位授予單位】：太原理工大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2017
【分類號(hào)】：TP391.44;TN929.5

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

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

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

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

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

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

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

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

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

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

本文編號(hào)：1400841