基于物理資源模型的物聯網軟件體系結構設計與形式化驗證

陳海明　崔莉　謝開斌

摘 要：實現眾多物理應用之間的互聯是建立物聯網的基本方法。然而，如何設計一種有效的架構指導物理應用的水平化互聯是目前物聯網研究領域尚未解決的問題之一。針對該架構設計問題，該研究組提出了一種支持物理應用水平化互聯的基于物理資源模型的物聯網軟件體系結構（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