计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2013年
6期
1185-1197
,共13页
物联网%物理应用%软件体系结构%物理模型%感执模型%应用模型
物聯網%物理應用%軟件體繫結構%物理模型%感執模型%應用模型
물련망%물리응용%연건체계결구%물리모형%감집모형%응용모형
IoT%physical applications%software architecture%physical model%sense-execute model%application model
实现众多物理应用之间的互联是建立物联网的基本方法.然而,如何设计一种有效的架构指导物理应用的水平化互联是目前物联网研究领域尚未解决的问题之一.针对该架构设计问题,提出了一种支持物理应用水平化互联的物理模型驱动的物联网软件体系结构(PMDA).PMDA由3个模型组成,分别是物理模型、感执模型和应用模型.模型之间以及模型内的组件之间通过连接器进行连接与交互,模型或组件在交互时需要满足一定的约束条件.通过体系结构描述语言Wright对PMDA中的3个模型的组成以及模型之间的交互进行了形式化描述.通过一种形式化验证工具PAT验证了用Wright描述的PMDA可以保证水平化互联起来的物理应用的有效性,即不存在死锁、发散和中止这3个影响物理应用有效互联的性质.基于PAT的验证结果,通过数学归纳法证明了根据PMDA开发的物联网应用系统在交互时不存在死锁、发散和中止的情形.
實現衆多物理應用之間的互聯是建立物聯網的基本方法.然而,如何設計一種有效的架構指導物理應用的水平化互聯是目前物聯網研究領域尚未解決的問題之一.針對該架構設計問題,提齣瞭一種支持物理應用水平化互聯的物理模型驅動的物聯網軟件體繫結構(PMDA).PMDA由3箇模型組成,分彆是物理模型、感執模型和應用模型.模型之間以及模型內的組件之間通過連接器進行連接與交互,模型或組件在交互時需要滿足一定的約束條件.通過體繫結構描述語言Wright對PMDA中的3箇模型的組成以及模型之間的交互進行瞭形式化描述.通過一種形式化驗證工具PAT驗證瞭用Wright描述的PMDA可以保證水平化互聯起來的物理應用的有效性,即不存在死鎖、髮散和中止這3箇影響物理應用有效互聯的性質.基于PAT的驗證結果,通過數學歸納法證明瞭根據PMDA開髮的物聯網應用繫統在交互時不存在死鎖、髮散和中止的情形.
실현음다물리응용지간적호련시건립물련망적기본방법.연이,여하설계일충유효적가구지도물리응용적수평화호련시목전물련망연구영역상미해결적문제지일.침대해가구설계문제,제출료일충지지물리응용수평화호련적물리모형구동적물련망연건체계결구(PMDA).PMDA유3개모형조성,분별시물리모형、감집모형화응용모형.모형지간이급모형내적조건지간통과련접기진행련접여교호,모형혹조건재교호시수요만족일정적약속조건.통과체계결구묘술어언Wright대PMDA중적3개모형적조성이급모형지간적교호진행료형식화묘술.통과일충형식화험증공구PAT험증료용Wright묘술적PMDA가이보증수평화호련기래적물리응용적유효성,즉불존재사쇄、발산화중지저3개영향물리응용유효호련적성질.기우PAT적험증결과,통과수학귀납법증명료근거PMDA개발적물련망응용계통재교호시불존재사쇄、발산화중지적정형.
