随着物联网系统的广泛应用,复杂的应用场景可能会导致物联网系统错误运行,为了避免给用户带来损害,在系统部署之前,如何使用统一、高效的方法进行系统地建模、验证成为目前亟待解决的一个重要问题。针对物联网系统中的异构特性,基于面向服务的思想,用统一的服务接口为用户提供需求,使物联网系统服务化,以服务的形式描述设备的功能。而在REST(Representational State Transfer,表述性状态转移)架构风格中,任何可被命名的信息都可被抽象为资源。由于REST式服务形式简单、设计轻量等特点,REST的设计更适合于资源受限的物联网服务设备。因此,基于REST中面向资源的核心思想,如何对物联网系统进行抽象建模成为首要问题。其次,想要在系统部署之前及时发现服务漏洞,还需要对模型进行验证分析。通信顺序进程(Communication Sequential Processes,CSP)是描述分布式并发软件系统规格和设计的一种典型的进程代数方法,由于物联网系统是一种分布式并发系统,基于物联网服务模型可以有效提高形式化分析和验证的效率,因此,将进程代数CSP方法应用到物联网服务模型的分析和验证中,有效地确保物联网服务的正确性和安全性显得尤为重要。本文针对以上问题,以物联网系统-室内空气质量服务为例,采用进程代数的形式分析方法进行建模与验证。主要内容如下:首先,根据物联网服务的分类,提出室内空气质量服务组成框架,并在此基础上,又提出物联网服务按需提供框架;然后,基于面向资源的思想,提出面向资源的物联网服务模型,针对标签迁移系统、并发系统、实时系统、概率通信顺序进程系统、概率实时系统这五种系统,对物联网服务的行为进行建模与分析,实现了对空气质量服务的快速形式化描述;最后,利用PAT模型检测器对该物联网服务的无死锁性、无发散性、确定性、可达性、活性这五种关键性质进行验证。通过对特定物联网应用场景的建模与验证,实验表明在PAT模型检测器上高效地验证了该服务的正确性和安全性。