陳海明　崔莉　謝開斌

摘 要：實現(xiàn)眾多物理應用之間的互聯(lián)是建立物聯(lián)網(wǎng)的基本方法。然而，如何設計一種有效的架構指導物理應用的水平化互聯(lián)是目前物聯(lián)網(wǎng)研究領域尚未解決的問題之一。針對該架構設計問題，該研究組提出了一種支持物理應用水平化互聯(lián)的基于物理資源模型的物聯(lián)網(wǎng)軟件體系結構（PMDA）。PMDA由三個模型組成，分別是物理模型、感執(zhí)模型和應用模型。模型之間以及模型內(nèi)的組件之間通過連接器進行連接與交互，模型或組件在交互時需要滿足一定的約束條件。通過體系結構描述語言Wright對PMDA中的三個模型的組成以及模型之間的交互進行了形式化描述。通過一種形式化驗證工具PAT驗證了用Wright描述的PMDA可以保證水平化互聯(lián)起來的物理應用的有效性，即不存在死鎖、發(fā)散和中止這三個影響物理應用有效互聯(lián)的性質(zhì)。基于PAT的驗證結果，通過數(shù)學歸納法證明了根據(jù)PMDA開發(fā)的物聯(lián)網(wǎng)應用系統(tǒng)在交互時不存在死鎖、發(fā)散和中止的情形。

關鍵詞：物聯(lián)網(wǎng) 物理資源模型 物聯(lián)網(wǎng)軟件 物理模型 感執(zhí)模型

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