陈海明　崔莉　谢开斌

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

关键词：物联网 物理资源模型 物联网软件 物理模型 感执模型

Abstract：It is a basic method to establish Internet of Things（IoT） by interconnecting all existing physical applications. However， there has not yet been an effective architecture to guide horizontal interconnections of physical applications. To address the problem， this paper proposes a software Architecture for Internet of Things based on Physical Resource Model （PMDA）， which supports the horizontal interconnections of physical applications. PMDA is composed of three models， namely， Physical Model， Sense-Execute Model and Application Model. The connections and interactions between models， and interactions among components in the models are realized by connectors， which satisfy some certain constraints. The composition of the three models in PMDA and the interactions among the models are formally described by an Architecture Description Language named Wright. The effectiveness of horizontal interconnections of physical applications based on PMDA is verified by PAT， in terms of deadlock-free， divergence-free and nonterminating. Besides that， those properties of IoT application systems developed under guidance of PMDA are proven by mathematical induction.

Key Words：IoT；PMDA；Physical Model；Sense-Execute Model；Application Model；Architecture Description Language

閱读全文链接（需实名注册）：http：//www.nstrs.cn/xiangxiBG.aspx？id=32688&flag=1