中文摘要：

物联网服务的建模和验证是当前物联网服务提供中的一个重要问题．文中将物联网服务的行为建模为其与相关环境实体的交互，并引入环境实体以刻画物理世界各种物体的属性和行为，从而将物联网服务能力建模为它能够导致的环境实体发生的期望变化．文中以时间自动机为建模工具，分别为将要监测和要控制的物理环境实体以及不同种类的物联网服务独立建模，以表现它们的独立性和自主性．这些时间自动机形成一个网络，刻画完整的物联网服务的通信并发过程，物联网服务的实施过程表现为时间自动机网络上的状态变迁通路．最后，文中提出一组物联网服务要满足的性质，并利用模型检测工具UPPAAL验证物联网服务的正确性．

英文摘要：

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 be- haviors of an IOT service are specified by its interaction with the corresponding environment enti- ties, 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 repre- sented 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.