基于实时UML顺序图的物联网交互模型

物联网是一个集计算、通信和控制于一体的智能系统,它通过监控和收集物理进程信息并将这些信息进行计算和分析,最终生成正确的控制指令用以执行,从而使物理环境变得更加安全和可靠。在物联网中,各物体通过网络连接或者本地连接的方式进行交互,这些交互具有时间性和地域性。物联网的建模和验证是物联网研究中一个重要的领域。文中提出一种基于实时UML顺序图的物联网交互模型,该模型将物联网中所有参与交互的物体建模为交互对象,并且通过实时UML顺序图对交互对象间的交互进行建模。使用时间自动机对交互对象的内部状态变化进行建模,以形成对交互模型的补充。最后根据转换规则将交互模型转换为时间自动机的形式以便于验证。通过一个实例,显示了如何具体应用物联网交互模型。进一步提出了物联网系统应该满足的一些性质,并使用UPPAAL模型检测工具对物联网交互模型进行分析和验证。

Interaction Model for Internet of Things Based on Real-time UML Sequence Diagram

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.