Modeling and verifying services of internet of things based on timed automata

作者：Li Li Xing; Jin Zhi^*; Li Ge

来源：Chinese Journal of Computers, 2011, 34(8): 1365-1377.

DOI：10.3724/SP.J.1016.2011.01365

• Environment entity
• Internet of things
• Internet of Things services
• Model checking tools
• Modeling approach
• Physical world
• Service modeling
• Timed Automata

The modeling and verifying of Internet of Things (IOT) services is now an important aspect of IOT software design. First, we introduce the concept of environment entities that are used to describe both the attributes and behaviors of things in the physical world. Then the behaviors of an IOT service are specified by its interaction with the corresponding environment entities, these interactions lead to the expected changes on the entities, and show the effectiveness of the IOT services. Based on timed automata, an IOT services modeling approach is proposed, in which different kinds of environment entities and IOT services are all modeled as individual timed automata. All these timed automata come into a network that represents the communication and concurrency of the whole IOT system, in which, the running of the IOT services will be represented as some computation path in the network. Based on the proposed approach, we present the properties with which the IOT services should be satisfied. By using the model-checking tool UPPAAL and the environment entities, we also present a verification approach for the correctness of IOT services models.

• 出版日期2011
• 单位中国科学院大学; 中国科学院数学与系统科学研究院; 北京大学