物联网被誉为是继计算机、互联网之后的第三次信息技术革命，已经引起各国政府、工业界和学术界的高度关注。随着以RFID、无线传感网络为代表的感知技术和通信技术的飞速发展，有许多物联网系统投入实际部署和运行，它们广泛应用于工业生产、环境监测、远程医疗、军事等领域，实时采集到大量现实世界的各种数据，人们通过分析这些数据，可以全面感知现实世界。物联网系统还可以通过各种控制设备和智能设备，如车载设备、医疗设备、手机等，影响和作用于现实世界。一个更进一步的问题是，如何在感知物理世界的基础上，使各种设备能够协同合作，持续地、及时地、动态地向现实世界提供人们期望的智能化服务。服务计算的思想是有可能成为应对这个问题的一个解决方案，物联网服务正是服务计算与物联网技术的结合，其核心思想是将异构的物理设备所提供的能力进行统一的封装，向外界提供服务。这样，利用物联网服务，人们就可以方便快捷地利用物理设备的能力，并将它们无缝地整合到上层业务流程中，从而构造出按需服务的物联网应用系统。物联网服务使现实世界和信息世界融合在一起，但是，如何对物联网服务进行抽象描述和性能分析，保障服务提供的正确性、可靠性、以及遵循物理设备特有其它性质，成为了一个亟需应对的问题。相比于传统的Web服务和软件服务，物联网服务借助于物理设备，并与物理环境直接交互。由于物理环境的约束，物联网服务受到服务的实时性要求高，服务提供设备可靠性低且服务资源受限等约束，服务计算中一些关于服务描述和分析的方法无法直接应用，需要构建适合物联网服务的新的建模、分析方法和技术。本文针对物联网服务的描述和性能分析问题，在物联网服务的建模框架、物联网服务的描述语言、物联网服务的行为和服务质量分析等三个方面上进行了深入的研究，取得了如下研究结果：　　 ⑴提出基于环境模型的物联网服务建模框架。不同于一般的Web服务和软件服务，物联网服务的能力与其所感知和作用的现实环境密切相关，物联网服务具有很强的环境依赖性，在满足用户需求的时候需要遵循现实环境的因果性，并满足环境约束。通过对多个实际物联网系统的应用场景和系统架构进行分析，本文提出基于环境的物联网服务建模框架，该框架将物联网服务要感知和作用的现实环境，显示地建模为一组环境实体，以及这组环境实体的变化规律。以这种环境模型为基础，该框架将物联网服务的能力需求和性能约束分别刻画为对环境实体的作用和环境实体对服务的约束和限制，支持服务能力的有效性验证和服务性能的满足性验证。本文给出了基于环境模型的物联网服务建模框架的概念模型，并提出了一组建模原则。　　 ⑵设计了基于环境模型的物联网服务建模语言。为了给物联网服务和现实环境提供一种统一的描述方法，本文设计了一种物联网服务的建模语言IoTSML。该语言具有如下特性：不依赖于任何程序设计语言和硬件平台，具有高度抽象性；不仅包含对物联网服务的描述，而是包含对现实环境和用户期望性质的刻画；不仅关注物联网服务的功能行为，而且对多种服务质量属性（如时间相关属性、可靠性、资源消耗等）均有相应的表达原语；提供对物联网服务间的通信和并发行为的描述能力，具有严格的基于概率时间自动机的语义解释。IoTSML的抽象性和严格的形式化语义，为物联网服务的能力分析和性质验证提供了基础。　　 ⑶提出了基于进程代数的物联网服务行为建模和分析方法。提出一种新的进程代数CCS-CASL，该进程代数结合了标准代数规格说明语言CASL和经典进程代数CCS。相比于大多数经典进程代数，CCS-CASL不但能表示并发系统的动态行为，而且可以描述系统中的静态数据部分。利用CCS-CASL，物理环境实体和物联网服务的行为均被建模为进程。服务与环境之间的数据传输、数据操作通过CCS-CASL的操作语义以形式化的方式表达出来。在此基础上，物联网服务在特定环境中的行为等价性被表示为一种强互模拟关系。这一表达方法的最大优点在于，结合物理环境的变化来分析物联网服务行为，更符合物联网服务随环境而动态变化的特性。该关系的一些重要性质，如等价性、同余性等，也在文中一一证明。这为物联网服务的行为匹配、替换等问题提供了一套严格而准确的描述和分析方法。　　 ⑷提出了一种物联网服务质量的建模和分析方法。现实环境从时间、地理位置、资源、动态变化性等方面对物联网服务的提供施加约束，这些约束使得关于服务质量的描述和分析变得愈发突出和重要。本文针对物联网服务三个重要的服务质量属性:时间相关属性、可靠性、资源消耗，分别以合适的形式化方法对它们进行建模和分析。(a)时间相关属性。本文以时间自动机为建模工具，分别为被感知和被控制的物理环境实体以及不同种类的物联网服务独立建模，表现出它们行为中与时间相关的属性和约束。这些时间自动机形成了一个网络，刻画出完整的服务和环境实体的通信并发过程，环境实体的自主变化、物联网服务的执行过程表现为时间自动机网络上的状态迁移路径。物联网服务与时间相关的性质以时序逻辑TCTL来表达，并通过模型检测工具UPPAAL验证这些性质的正确性。(b)可靠性和资源消耗。本文将这两种有紧密联系的属性放在一起研究，以带代价结构的马尔可夫决策过程为建模工具，同时刻画出物联网编配式服务组合的可靠性和资源消耗。与可靠性和资源消耗相关的服务组合性质以概率时序逻辑PCTL的逻辑公式来描述，最后通过概率模型检测工具PRISM在服务组合模型上对这些性质进行验证和分析。　　 ⑸从实际物联网系统的系统架构出发，归纳出物联网服务的建模关注点，提出基于环境的物联网服务建模框架。在此框架下，本文构建出一种物联网服务建模语言IoTSML，使各类物联网服务和物理环境具有了一个统一的模型描述。更进一步地，本文将物联网服务的描述从功能行为和多种服务质量属性等多角度进行解析，分别采用进程代数、自动机、模型检测等形式化方法和工具进行服务性质的自动化验证和分析。未来研究工作将重点关注于本文所提出方法在实际物联网场景中的应用，以及物联网服务的动态性、安全性、私密性等特性的建模和分析。