Quantitative Verification Methodology On Internet-of-things Interactive System

With the realization of the new generation of network technology and hardware devices,the Internet of Things(IoT)technology has been researched and developed unprecedentedly,and its application has gradually entered the stage of marketization,from smart cities,field research workstations,to miniature heart rate control systems.Any object on the earth can become an integral part of the IoT,so the scale of the IoT will be quite large,and its implementation difficulty and interaction mechanism will increase dramatically.At the design level,ensuring the correctness of IoT applications becomes a key and difficult point.From the perspective of software engineering,this paper abstracts the various components of the IoT into independent components with interfaces according to the design principle of “high cohesion and low coupling”,focusing on the correctness and rationality of communication interaction between components,and studies the resulting IoT interactive system.This paper uses the formal method to establish an appropriate model for the characteristics of the IoT interactive system,and verify the quantitative properties that the system should satisfy in terms of non-functional requirements such as probability,time,cost,and data flow.This provides a formal method for analyzing and verifying the IoT interactive system.The main innovations of this paper are as follows:1.A formal description model of the IoT interaction system is established.Aiming at the flexible network topology of IoT interaction system and the characteristics of communication interaction,this paper selects Reo communication model as the formal modeling language.According to the characteristics of the IoT interaction system,the expression ability of probability,time and cost is extended on the basis of Reo,forming a whole model.The formal description model of the IoT interaction system,called cost probability time Reo,is proposed.At the same time,its semantic model,called cost probability time constrained automaton(pPTCA),is given,and so is the correspondence between these two.People can easily model the IoT interaction system by our model,and use the corresponding semantic model to perform related formalverification and analysis.2.A logic system is constructed to describe the natural properties of the IoT interactive system.In view of the price,probabilistic,timed,and non-deterministic characteristics of the IoT interactive system,this paper selects extended probabilistic computation tree logic as the basic logic.Considering that the communication interaction in the IoT interactive system is data-driven and the importance of resources,the ability to express the data flow and the cost behavior is extended in this logic to specify the properties of the IoT interaction system,forming priced probabilistic timed scheduled data stream logic(pPTDL).In order to integrate the Modest tool for automatic verification, this paper studies the conversion from the simplified pPTCA to the stochastic timed automaton that supports the action set,and establishes the theoretical basis of using the tool.3.The behavioral equivalence of the IoT interactive system model is studied.The sheer size of the IoT interactive system leads to a large-scale formal model, which will bring great difficulties to quantitative verification and analysis.In order to reasonably reduce the scale of the model,this paper adopts the classical mutual bisimulation technology,and gives the corresponding strong bisimulation and weak bisimulation research from the perspective of whether or not to consider the internal behavior of the system.For strong bisimulation,this paper extends the equivalence constraints on probabilistic behavior,time behavior,and cost behavior.For the weak bisimulation,this paper focuses on the probabilistic model,and considers the important influence brought by the divergent behavior(i.e.,infinite sequence of internal behavior).The theoretical definition of divergence-preservation weak probabilistic bisimulation and the corresponding verification method are studied from three angles.By combining inductive idea and classical refinement method,this paper designs a polynomial-time algorithm for computing the coarsest divergence-preservation weak probabilistic bisimulation.4.This paper describes a case of the IoT interactive system,i.e.,a small field workstation working independently in remote environments.By applying the model and logic proposed in this paper,the system is modeled,the properties are specified,and the corresponding quantitative verification and analysis are completed.This case demonstrates the effectiveness of the proposed method for quantitative verification of IoT interactive systems.