物联网融合了物理世界和信息世界,延伸和扩展了互联网,成为了大家研究的热门领域。随着物联网的快速发展,物联网也变得越来越复杂,使得现有对物联网的研究已经有了局限性。一方面,由于物联网中的设备直接运行于物理环境中,需要同物理环境进行直接交互。物理设备的运行和物理环境的改变通常是连续变化的,而对物理设备的控制常常是离散指令。目前对物联网的研究在这一特性上考虑不够,主要采用模型检查方式的验证,在处理连续变化时可能遇到状态爆炸的情况。另一方面,物联网中用到的物理设备越来越多,使物联网的规模变得越来越庞大,内部交互越来越复杂。目前对物联网的研究,主要是对物联网进行整体的分析,既不便于扩展和维护,其设计与验证过程也较为复杂。混成系统(Hybrid Systems)是一类同时包含连续动态行为和离散动态行为的系统。混成系统的建模方法同时具有离散和连续的刻画能力,能够较好的描述物联网系统的离散指令和物理设备的连续行为,很好的符合了物联网的特点。近年来,Andre Platzer等提出了以微分动态逻辑为基础的混成系统建模与验证方法,取得了很好的研究成果,同时开发了混成系统自动验证工具KeYmaera。针对分布式混成系统,微分动态逻辑后续又扩展为定量微分动态逻辑,在公式中引入了定量算子,支持分布式混成系统的建模,验证工具也升级为KeYmaeraD,大大提高了原有模型的扩展与应用能力。本文结合物联网的特点,提出了一套对物联网系统进行服务建模的方法,贯穿物联网系统的模拟、组件化建模和验证的整个过程,很好的贴合了物联网系统越来越庞大,内部交互越来越复杂的特点。本文先将一个复杂的物联网系统根据功能封装成若干个小的成员服务,然后用Ptolemy Ⅱ分别对成员服务进行可视化的设计和模拟,利用混成自动机作为桥梁,将设计图转化为混成程序,用混成系统对成员服务进行组件化建模,最后通过对成员服务进行组合的方式将成员服务合成一个整体服务。这种分而治之的方法,具有良好的模块性,保证了物联网系统的可扩展性。而对物联网服务的验证,也可受益于这种模块化的思想。本文中使用微分动态逻辑对物联网服务进行验证。验证的过程也是自顶向下,我们将整体的验证目标分解为针对成员服务的子目标,以减小问题的规模。然后我们使用KeYmaera辅助,对分配给成员服务的子目标进行验证,这样可以通过研究成员服务的性质来研究整个服务的性质。