Research On The Combination And Verification Of Internet Of Things

Internet of Things (IoTs) combines the physical world and the world of infor-mation. As an extension of the Internet, it has become a popular research topic. With the rapid development of the IoTs, it becomes increasingly complex, making the ex-isting research on the IoTs no longer appropriate. First, physical equipment run di-rectly in the physical environment, and need to interact with the physical environment. The equipment and the environment typically changes continuously, and the control of the physical devices are often discrete instructions. The current research consider little for this feature, and use model checking for verification, which may lead to state explosion when dealing with continuous change. Second, more and more physical de-vices are used in IoTs, which makes the scale of IoTs increasingly large and internal interaction increasingly complex. The current researches of IoTs focus on overall analysis, which is hard to extend and maintain, and also makes the design and verifi-cation process much more complicated.Hybrid systems are systems combine continuous dynamics and discrete dynam-ics. The hybrid system can model both discrete and continuous changes, which suit the Internet of Things well. In recent years, Andre Platzer proposed the differential dynamic logic based hybrid system modeling and verification method, and achieved good results. They also developed a hybrid system verification tools KeYmaera. To support distributed hybrid system, they proposed quantified differential dynamic logic, which introduced quantified operators into formulas. KeYmaera also upgrade to KeYmaeraD. These researches greatly improved the modeling capabilities.According to the characteristics of the Internet of Things, we proposed a service based modeling method for Internet of Things. This modeling method runs through the whole process of IoTs, from simulation, modeling to verification, and it fits well for big IoTs systems with complex internal interaction.In this paper we first encapsulate a complex IoTs system to several sub services, and then use Ptolemy II to design and simulate them visually. We use of hybrid au-tomata as a bridge, to convert the design into hybrid program. Then we can model the sub services as components, and composite the sub services into a whole service. This divide-and-conquer method ensures the modularity and scalability of the IoTs sys-tems. Verification of the IoTs also benefit from this modular method. Differential dy-namic logic is used in this article. The verification process is top-down, our overall verification goals are broken into several sub-goals of the sub systems, to reduce the scale of the problem. Then we use KeYmaera to verify these sub-goals. In this way, we can verify the whole systems by verify their sub systems.