The Formal Modeling And Verification Of Resource-Oriented Internet Of Things System

With the development of IoT(Internet of Things)system,it has been widely used,but in complex application scenarios,IoT system may lead to run wrong operation.In order to reduce the damage caused by the systematic failure to the user,before the deployment of system,how to use an unified and efficient method to systematically design,model,verify IoT system becomes a problem to be solved at present.Aiming at the heterogeneous characteristics of IoT system,the users can use the unified interface of service to satisfy demand based on the service-oriented idea.The IoT system can be servitization which describes the function of the equipment in form of service.But,in architectural style of REST,any information that can be named can be abstracted as resources.Because the characteristics of restful service are simple form and lightweight design,the design of REST is more suitable for resource-constrained IoT equipment.Therefore,how to model and verify IoT system abstractly becomes the primary issue based on the resource-oriented idea of REST.Secondly,if we want to find the vulnerabilities of services in time before the system deployment,we also need to verify and analyze this model.Communication Sequential processes area method of typical process algebra to describe specification and design of the distributed and concurrent software system.Because IoT systems are distributed and concurrent systems,and the model of Iot service can effectively improve the efficiency of the formal analysis and verification.In order to effectively ensure correctness and security of IoT services and use the method of CSP to analyze and verify IoT services are particularly important.In view of the above problems,the example of this paper is IoT system-indoor air quality service,with the analytic method of process algebra for modeling and verification.First of all,according to the classification of IoT service,we come up with the framework of the components in air quality services,and based on it,we propose the offered framework of the IoT services.Secondly,based on the resource-oriented idea,a model of resource-oriented IoT services is put forward.And the detecting systems contain labeled transition system,real-time system,communication sequential processes,probability communication sequential processes,probability real-time system,the behaviors of IoT service are modeled and analyzed for these five kinds of systems.So it has realized formal description of air quality services.Finally,we use PAT tool to verify the five key properties of IoT services,including deadlock,divergent,deterministic,reachability,liveness.Through analyzing specific IoT applied scenarios,the experiment proves the correctness and security of service.