实现众多物理应用之间的互联是建立物联网的基本方法．然而，如何设计一种有效的架构指导 物理应用的水平化互联是目前物联网研究领域尚未解决的问题之一．针对该架构设计问题，提出了一种 支持物理应用水平化互联的物理模型驱动的物联网软件体系结构（PMDA）．PMDA由3个模型组成， 分别是物理模型、感执模型和应用模型．模型之间以及模型内的组件之间通过连接器进行连接与交互， 模型或组件在交互时需要满足一定的约束条件．通过体系结构描述语言Wright对PMDA中的3个模 型的组成以及模型之间的交互进行了形式化描述．通过一种形式化验证工具PAT验证了用Wright描 述的PMDA可以保证水平化互联起来的物理应用的有效性，即不存在死锁、发散和中止这3个影响物 理应用有效互联的性质．基于PAT的验证结果，通过数学归纳法证明了根据PMDA开发的物联网应用 系统在交互时不存在死锁、发散和中止的情形．
