面向资源的物联网系统形式化建模与验证

发布时间：2018-01-09 09:21

本文关键词：面向资源的物联网系统形式化建模与验证　出处：《太原理工大学》2017年硕士论文　论文类型：学位论文

【摘要】：随着物联网系统的广泛应用,复杂的应用场景可能会导致物联网系统错误运行,为了避免给用户带来损害,在系统部署之前,如何使用统一、高效的方法进行系统地建模、验证成为目前亟待解决的一个重要问题。针对物联网系统中的异构特性,基于面向服务的思想,用统一的服务接口为用户提供需求,使物联网系统服务化,以服务的形式描述设备的功能。而在REST(Representational State Transfer,表述性状态转移)架构风格中,任何可被命名的信息都可被抽象为资源。由于REST式服务形式简单、设计轻量等特点,REST的设计更适合于资源受限的物联网服务设备。因此,基于REST中面向资源的核心思想,如何对物联网系统进行抽象建模成为首要问题。其次,想要在系统部署之前及时发现服务漏洞,还需要对模型进行验证分析。通信顺序进程(Communication Sequential Processes,CSP)是描述分布式并发软件系统规格和设计的一种典型的进程代数方法,由于物联网系统是一种分布式并发系统,基于物联网服务模型可以有效提高形式化分析和验证的效率,因此,将进程代数CSP方法应用到物联网服务模型的分析和验证中,有效地确保物联网服务的正确性和安全性显得尤为重要。本文针对以上问题,以物联网系统-室内空气质量服务为例,采用进程代数的形式分析方法进行建模与验证。主要内容如下:首先,根据物联网服务的分类,提出室内空气质量服务组成框架,并在此基础上,又提出物联网服务按需提供框架;然后,基于面向资源的思想,提出面向资源的物联网服务模型,针对标签迁移系统、并发系统、实时系统、概率通信顺序进程系统、概率实时系统这五种系统,对物联网服务的行为进行建模与分析,实现了对空气质量服务的快速形式化描述;最后,利用PAT模型检测器对该物联网服务的无死锁性、无发散性、确定性、可达性、活性这五种关键性质进行验证。通过对特定物联网应用场景的建模与验证,实验表明在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

【相似文献】