基于物理資源模型的物聯(lián)網(wǎng)軟件體系結(jié)構(gòu)設(shè)計(jì)與形式化驗(yàn)證

陳海明　崔莉　謝開(kāi)斌

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

關(guān)鍵詞：物聯(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

閱讀全文鏈接（需實(shí)名注冊(cè)）：http：//www.nstrs.cn/xiangxiBG.aspx？id=32688&flag=1