关键词: 物联网,交互模型,实时UML顺序图,时间自动机,验证

Abstract: Internet of things (IOT) is an intelligent system which integrates computation,communication and control.It aims at monitoring the behavior of physical processes,analyzing information to generate correct instructions,and actuating actions to make physical environment work correctly and better.In Internet of things,different things interact locally or through network connections.These interactions are affected by time and locations.Modeling and verification of Internet of things are an important area in the research of Internet of things.This paper proposed an interaction model for IOT based on real-time UML sequence diagram.In our model,all things that interact in IOT are modeled as interactive objects between which interactions are modeled by real-time UML sequence diagram.And timed automata is used to model the internal state changes of interactive objects,which results in a complement to the interaction model.Finally according to the transition rules,the interaction model was transformed to the form of timed automata for the sake of verification.A case study was used to show how to specifically apply the interaction model.Further some properties which IOT should satisfy were presented.And the model checking tool UPPAAL was used to analyze and verify the interaction model for IOT.

Key words: Internet of things,Interaction model,Real-time UML sequence diagram,Timed automata,Verification