随着新一代网络技术和硬件设备的实现,物联网(Internet of Things)技术得到了空前地研究和发展,其应用也逐步进入市场化阶段,从智慧城市,野外考察工作站,到微型心率控制系统等。地球上的任何一个物体都可以成为物联网的组成部分,因此物联网的规模将会相当庞大,其实现难度以及交互机制的复杂性也会急剧增加。在设计层保证物联网应用的正确性成为关键和难点。本文从软件工程角度出发,根据“高内聚低耦合”的设计原则,将物联网各个组成单元抽象为具有接口的独立组件,侧重于组件之间通信交互的正确性、合理性,研究由此形成的物联网交互系统。人们通常从测试的角度研究一个系统的可执行性,但这样并不能保证该系统的正确性。本文使用形式化方法,针对物联网交互系统具有的特征进行建模,并从概率、时间、代价、数据流等非功能性需求方面对系统应满足的性质进行量化验证分析,从而保证系统运行的正确性。以此提供了一种对物联网交互系统进行分析验证的形式化方法。本文主要工作和创新点有以下四个方面:1.建立了物联网交互系统的形式化描述模型。针对物联网交互系统灵活多变的网络拓扑结构,以及以通信交互为主的特性,本文在Reo通信模型基础上扩展概率、时间、代价等方面的表达能力,提出物联网交互系统的形式化描述模型——Reo。进一步给出该模型的语义模型——pPTCA。人们可以很方便地通过描述模型对物联网交互系统进行建模,同时利用对应的语义模型进行相关的形式化验证分析。2.构建了物联网交互系统性质的逻辑表达系统。为了规范代价约束、概率性、时间性等物联网交互系统的特征,本文选取作为基础逻辑。考虑到物联网交互系统中资源的重要性以及通信交互的数据驱动性,在该逻辑上分别扩展数据流及代价行为的表达能力,构建了物联网交互系统性质的刻画逻辑——pPTDL。为了集成Modest工具进行自动化验证,本文研究了从pPTCA的反应式模型到支持动作集的随机时间自动机的转换机制,为该工具的使用提供了理论支撑。3.研究了物联网交互系统模型的互模拟等价。物联网交互系统规模的庞大必然导致形式化模型的复杂,这将给量化验证分析带来极大的困难。为了合理约减模型的规模,本文从是否考虑系统内部行为的角度,分别对强互模拟以及弱互模拟进行研究。针对强互模拟,本文研究具有概率、时间、代价等特征的约束自动机模型的行为等价。针对弱互模拟,本文侧重于概率模型,并考虑到发散行为(即无限内部行为)所带来的重要影响,从三个角度研究了保发散弱概率互模拟的相关理论以及对应的验证方法。通过结合归纳思想以及经典剖分精化方法,本文设计了计算最大保发散弱概率互模拟的多项式时间算法。4.介绍了偏远环境下独立工作的小型野外工作站物联网交互系统案例。通过应用本文提出的模型与逻辑,对该物联网交互系统进行建模并对其具有的性质进行逻辑规范,在此基础上完成量化验证与分析,从而表明了本文提出物联网交互系统量化验证方法的有效性。