随着通信技术与智能设备的飞速发展,物联网系统在许多领域具有广泛的应用,已成为学术界和工业界的重要研究与应用领域。但随着物联网系统功能趋于复杂、应用领域不断扩展,物联网系统面临着应用复杂化,运行环境不确定等问题。物联网系统需要保证其在面对不确定性环境,物联网本身复杂的结构与通信,仍能保持系统的实时性和规范性,对外界的不确定因素进行正确的反应和处理,本文针对上述问题,对物联网系统运行环境中不确定性环境因素的推理,以及不确定环境下物联网系统服务的形式化建模与验证工作进行了研究。首先,提出基于情景本体的动态模糊贝叶斯不确定性推理算法。情景本体将不确定性环境抽象成情景概念,建立各个环境影响因素的概念与关联。通过情景本体与贝叶斯网络之间结构的共性,结合环境本身实时变化、因果关系难以用特定数值描述等特点,提出了使用动态模糊贝叶斯网络推理环境因素的算法,并且给出了情景本体到动态模糊贝叶斯网络的转换方法,然后推理说明了算法的有效性。其次,构建了基于概率时间自动机的物联网服务模型。通过周围环境变化的推理,系统服务需要对变化进行相应推理和处理,使服务运行仍符合原有需求规范和功能要求。对物联网系统开展形式化建模与验证,以保证整个系统的实时运行性和服务可用性,以及规范的满足性。本文使用概率时间自动机对服务化的物联网系统进行建模,将外界环境、物理设备、物联网服务分别根据其特点进行建模,并且基于时间通信顺序进程TCSP对模型进行形式化表示,便于性质的验证工作。最后,对基于服务的物联网系统建立的模型构建了应用原型。为了说明遵从物联网系统的实时性和规范性,采用了智能停车场系统,给出了不确定环境下需要满足的无死锁性、一致性等性质描述,使用进程代数语言TCSP描述了系统模型中各个服务组件和关系,从而对整体进行了形式化建模。基于模型检测工具PAT对建立的模型进行了无死锁性、实时性、规范性、一致性的性质验证,结果表明本文提出的形式化建模方法可以有效的对物联网服务系统进行建模,并且能够保障在不确定环境中实时性和规范性方面应该满足的性质。