物联网的概念自1999年由麻省理工学院提出以来^[1],物联网在理论方面的研究^[2,3,4,5]和工程方面的实践^[6,7]越来越多,世界各国也制定了相应的政策来大力发展物联网^[8,9,10,11].物联网与传统的网络相比,最根本的区别是物联网要对物理环境进行感知,并根据感知信息和物联网用户的需求对物理环境进行控制^[12].

我们在之前的研究工作中提出了一种基于物理模型的物联网软件体系结构(PMDA)^[13].PMDA认为:物联网软件系统由多个相互关联的物理应用组成,每个物理应用由物理模型、感执模型和应用模型组成.物理模型是物理应用的感知基础和控制对象;应用模型提取用户对物联网的需求信息;感执模型连接物理模型和应用模型,实现了物理应用之间的水平互连和对物理环境的感知与控制.可见,感执模型是构建物联网软件的核心.为了最终达到将PMDA应用于物联网软件开发的目的,本文对PMDA中的感执模型(SEM)进行求精.求精后的感执模型称为R-SEM.

简要来讲,R-SEM考虑了物联网的特有属性,将SEM的内部构件按照物理应用的感执工作流程分解为用通信顺序进程(CSP)^[14]表达的子构件来说明构件端口的功能的实现,并采用CSP中的导管运算符说明子构件的端口与构件的端口之间的同步,通过CSP描述了子构件与子构件之间的交互.本文使用进程分析工具(PAT)^[15]对R-SEM进行了验证.验证的结果表明:R-SEM中子构件之间的交互、子构件的端口与构件的端口之间的同步保持了SEM所具有的保证物理应用之间有效互联的性质——不死锁、 不中止和不发散.由于R-SEM精化了SEM的内部组成,且保持了SEM的有效互联性质,因此,R-SEM对最终将PMDA应用于物联网软件的开发具有实际的指导意义.

本文第1节介绍物联网体系结构求精方面的相关工作.第2节简要介绍本文工作的研究背景,即,我们之前提出的一种基于物理模型的物联网软件体系结构(PMDA)和其中的感执模型(SEM).第3节说明感执模型的求精过程和求精后的感执模型(R-SEM).第4节对R-SEM进行验证.第5节对本文的工作进行总结.

目前,针对物联网软件已经提出了多种体系结构,其中,考虑了感执特征的体系结构主要有:(1) Guinard等人^[16]提出的基于SOA的物联网体系结构.该体系结构通过Web Service来组织物理世界中存在的物理服务,通过搜索机制查找与用户需求最匹配的物理服务,通过选择机制选取最符合用户需求的物理服务实例,如果查询不到能够满足用户需求的物理服务,还可以动态部署满足用户需求的物理服务.(2) Tsiatsis等人^[17]在SENSEI项目研究的基础上提出了物理资源的组织架构.该架构将物理资源的管理分成4层:无线感知与执行网络(WS&AN)物理资源层、统一资源接入及资源发现层、资源的语义查询和动态资源创建层、资源的执行管理和会话支持层.其中,WS&AN物理资源层,资源的执行管理和会话支持体现了物联网的感执特征.

对软件体系结构的求精是指,通过反复迭代的精化,最终达到软件体系结构在软件系统上实现的目的.目前,在软件体系结构求精方面所进行的研究还比较少,主要的研究成果有:(1) Oquendo等人^[18]提出的p-ARL体系结构精化描述语言,通过描述软件体系结构的端口、数据以及结构的精化活动,根据重写逻辑对软件体系结构逐步求精;(2) Abi-Antoun等人^[19]根据非传递无干扰理论,将构件分解成子构件,描述子构件之间基 于信息流的交互,提出了体系结构中不同精化层之间保持信息的语义完整性的策略.

在以前的研究工作中,我们提出了一种基于物理模型的物联网软件体系结构(PMDA).在该软件体系结构中,我们根据三元理论^[20]将物联网软件抽象为由多个相互关联的物理应用组成的系统,每个物理应用划分为3个部分,每个部分由一个模型构成,分别是应用模型(AM)、感执模型(SEM)和物理模型(PM).物理模型提供物理数据并对物理环境进行控制;应用模型实现对社会群体需求信息的提取;感执模型连接物理模型与应用模型,实现了物理应用之间的水平互联和对物理环境的感知与控制.

例如,以一个实现室内温度和亮度监控的智能家居物联网系统为例,实现一个房间监控功能的软件为一个物理应用,多个物理应用相互关联组成一个物联网软件系统.对每个物理应用而言,其中的应用模型描述了用户对室内温度和亮度的监控需求;物理模型描述了所监控的室内环境的温度和亮度状态以及对室内环境进行控制的执行构件,比如空调的温度调节和电灯的功率调节;感执模型根据用户的需求以及感知到的温度和亮度的信息,调用物理模型内的执行构件产生相应的控制命令调节本房间的环境状态,如果本物理应用的命令执行无法满足需求,将控制命令发送到其他物理应用,调节其他房间的环境状态,最终达到用户的需求.

从以上例子可以看出:通过物理应用之间的相互关联实现物联网软件系统,感执模型的设计最为关键.我们按照感执模型的工作流程把它定义为由6个构件组成,分别是需求判别构件(RDI)、需求分解构件(RDE)、外部应用关联构件(OAP)、感知构件(SEN)、物理数据处理构件(PRO)和决策执行构件(EXE).6个构件所要实现的功能描述如下:

1) 构件RDI接收应用模型处理后的需求信息,判别哪些需求可以由本应用完成,哪些需求不能由本应用完成,将本应用可以完成的需求发送给构件RDE,将不能完成的需求发给构件OAP.

2) 构件RDE接收构件RDI输出的需求信息以及其他外部应用发送的需求信息,并将这些需求信息分解为数据请求信息和控制请求信息.数据请求信息发送给构件SEN,控制请求信息发送给构件EXE.

3) 构件OAP接收构件RDI输出的需求信息,根据这些需求信息建立与外部应用的对应关系,并将需求信息发送给相应的外部应用,同时还能接收外部应用的请求.

4) 构件SEN接收构件RDE输出的数据请求信息,并根据数据请求信息从物理模型中获取感知数据,并将感知数据发送给构件PRO.

5) 构件PRO接收来自构件SEN的感知数据并进行处理,将处理后的信息发送给构件EXE.

6) 构件EXE接收构件RDE的控制请求信息和构件PRO发送的感知数据处理信息;根据控制请求信息与感知数据处理信息做出决策,产生决策执行信息,并将决策执行信息发送给物理模型.

图 1表述了感执模型的6个构件以及构件之间通过端口的连接关系.

图 1

Fig. 1

Fig. 1 Relationship of components in SEM图 1 感执模型的构件关系

基于SEM进行的物理应用和物联网软件开发,首先需要实现SEM的构件端口的功能,接着实现构件端口与端口之间的连接功能.在我们设计的基于物理模型的物联网软件体系结构(PMDA)中,给出了SEM中构件端口所应该具备的功能,但没有给出实现这些功能的具体内容,从而使得PMDA还不能应用于物联网的软件开发.为了最终达到软件体系结构应用于物联网软件开发的目的,需要对SEM进行求精.R-SEM实现了对 SEM的求精,求精在SEM的构件内部按照感执模型的工作流程、所具有的属性(空间属性、关联属性和动态属性)以及所具有的特征(感执特征、资源受限特征、数据异构特征和行业特征)分解为用CSP中的进程表达的子构件,以说明构件端口功能的实现.

R-SEM内每个构件的端口功能通过构件内部的子构件来实现,同时,构件的端口还与相应的子构件的端口保持同步.根据感执模型内的构件的工作流程,依次对感执模型内的每个构件进行求精,求精所采用的策略是根据构件在物理应用中所体现的属性特征.构件RDI根据物理应用的空间属性进行求精;构件RDE根据SEM本身具有的感执特征进行求精;构件OAP根据物理应用的动态性以及物理应用之间的关联性进行求精;构件SEN根据物理应用的感知资源受限特征进行求精;构件PRO根据物理应用中的感知数据的异构特征进行求精;构件EXE根据物理应用所归属的行业特征进行求精.模型R-SEM在求精过程中依据3个属性:空间属性、关联属性和动态属性以及4个特征:感执特征、资源受限特征、数据异构特征和行业特征.R-SEM内的子构件的功能使用CSP中的进程来描述,并通过事件来说明子构件之间以及子构件与构件的端口是如何同步的.最后,通过构件内部的交互图来形象地说明构件内部的组成以及子构件之间的交互.

我们用4种符号来表达R-SEM的基本组成元素,如图 2所示.

图 2

Fig. 2

Fig. 2 Basic elements in R-SEM图 2 R-SEM的基本元素

需求判别构件(RDI)通过端口P_{rdi_req}接收来自应用模型的需求;通过端口P_{rdi_ireq}向需求分解构件(RDE)提供本地需求信息;通过端口P_{rdi_oreq}向外部应用关联构件(OAP)提供与外部物理应用相关的需求信息.

构成物联网的物理应用具有空间属性,不同的物理应用所处的物理位置是不相同的.构件RDI的主要功能是判别需求信息中所包含的物理位置信息和物联网内的物理应用的物理位置信息之间的关系.我们通过对构件RDI实现的这一判别功能进行分解,实现对构件RDI的精化.精化后的判别构件(RDI)内部包括3个子构件:需求接收子构件(RR)、本地需求子构件(LR)和外部需求子构件(ER).这3个子构件分别对应需求判别子构件(RDI)的3个端口所提供的功能.

RR要实现如下的功能:接收来自构件RDI的端口P_{rdi_req}传送的的需求信息和LR发送的本地物理位置信息;比较需求的物理位置信息与本地物理位置信息,将与本地物理位置相关的需求信息发送给子构件LR,将与本地物理位置无关的需求信息发送给子构件ER.用CSP将RR要实现的功能抽象为如下的事件:事件recv_ereq表示接收从构件RDI的端口P_{rdi_req}传送的需求信息,事件ladd r表示接收LR发送的本地物理应用的物理位置信息,事件ext_paddr表示从需求信息中提取需求的物理位置信息,事件comp_addr表示对比需求物理位置信息与本地物理位置信息,事件lreq表示将与本地物理应用相关的信息发送给子构件LR,事件exreq将与外部需求相关的信息发送给子构件ER.用CSP可以将子构件RR表示为

PRR=recv_ereq→laddr→ext_paddr→comp_addr→lreq→exreq→PRR.

LR要实现如下的功能:更新本地物理应用的位置信息,接收子构件RR的需求信息,并将需求信息发送给构件RDI的端口P_{rdi_ireq}.LR所提供的功能用可以用CSP抽象为如下的事件:事件laddr表示更新本地物理应用的位置信息,事件lreq表示接收子构件RR发送的需求信息,事件send_inreq表示将本地需求信息发送给构件RDI的端口P_{rdi_ireq}.LR可以用CSP中的进程表示为

PLR=laddr→lreq→send_inreq→PLR.

ER要实现如下的功能:接收子构件RR发送的需求信息,并将需求信息发送给构件RDI的端口P_{rdi_oreq}.ER所提供的功能可以用CSP抽象为如下的事件:事件exreq表示接收子构件RR发送的需求信息,事件send_oreq表示将外部需求信息发送给构件RDI的端口P_{rdi_oreq}.ER可以用CSP中的进程表示为

PER=exreq→send_oreq→PER.

进程PRR与进程PLR在执行事件laddr和事件lreq时要进行同步,同步的端口分别为p1和p2.进程PRR与进程PER在执行事件exreq时要进行同步,同步的端口分别为p3和p4.进程PRR在执行事件recv_ereq时,通过端口p5与构件RDI的端口P_{rdi_req}进行同步.进程PLR在执行事件send_inreq时,通过端口p6与构件RDI的端口P_{rdi_ireq}进行同步.进程PER在执行事件send_oreq时,通过端口p7与构件RDI的端口P_{rdi_oreq}进行同步.

构件RDI求精后的结果如图 3所示.

图 3

Fig. 3

Fig. 3 Refinement in component RDI图 3 RDI构件求精

需求分解构件(RDE)通过端口P_{rde_req}接收来自构件RDI的本地需求信息,通过端口P_{rde_reqd}向感知构件(SEN)发送感知需求信息,通过端口P_{rde_reqc}向决策执行构件(EXE)发送控制请求信息.

物联网中的物理应用既要感知物理环境,又要对物理环境进行控制.我们通过分解物理环境感知以及控制过程,实现对构件RDE的精化.精化后的需求分解构件(RDE)内部包括3个子构件:需求分类子构件(RC)、感知类型子构件(SC)和控制类型子构件(CC),这3个子构件分别对应RDE的3个端口所提供的功能.

RC要实现如下的功能:接收构件RDE的端口P_{rde_req}传送的本地需求信息,接收来自OAP构件的外部需求信息,提取需求信息中的感知物理参数和需求信息中的控制参数,包括控制类型、控制值等.用CSP将RC要实现的功能抽象为如下的事件:事件recv_inreq表示接收RDE的端口P_{rde_req}传送的需求信息,事件recv_oap表示接收来自OAP的端口P_{oa_oap}传送的外部应用的需求信息,事件phy_par表示获取需求信息中的感知物理参数,事件creq表示获取需求信息中的控制需求参数.用CSP将子构件RC的行为表示为

PRC=recv_inreq→recv_oap→phy_par→con_req→PRC.

SC要实现如下的功能:接收子构件RC发送的感知物理参数,将同类型的物理参数归为一类,类型由物理应用自身拥有的物理参数类型决定.用CSP将SC要实现的功能抽象为如下的事件:事件phy_par表示接收物理参数,事件phy_cla表示将物理参数进行归类,事件send_datareq表示将物理参数所归属的类型传送给RDE的端口P_{rde_reqd}.用CSP将子构件SC的行为表示为

PSC=phy_par→phy_cla→send_datareq→PSC.

CC要实现如下的功能:接收子构件RC发送的控制需求;判断控制类型,对非精确控制类型,要给出一个符合要求的具体值;将具有明确意义的控制信息发送给构件RDE的端口P_{rde_reqc}.用CSP将CC要实现的功能抽象为如下的事件:事件creq表示接收子构件RC发送过来的控制需求,事件gen_conreq表示生成控制需求信息,事件send_conreq表示将控制需求信息发送给构件RDE的端口P_{rde_reqc}.用CSP将子构件CC的行为表示为

PCC=creq→gen_conreq→send_conreq→PCC.

进程PRC与进程PSC在执行事件phy_par时要进行同步,同步的端口分别为p8和p9.进程PRC与进程PCC在执行事件creq时要进行同步,同步的端口分别为p10和p11.进程PRC在执行事件recv_inreq时,通过端口p12和构件RDE的端口P_{rde_req}进行同步.进程PRC在执行事件recv_oap时,通过端口P_{oa_rde}与OAP的端口P_{oa_oap}进行同步.进程PSC在执行事件send_datareq时,通过端口p13和构件RDE的端口P_{rde_reqd}进行同步.进程PCC在执行事件send_conreq时,通过端口p14和构件RDE的端口P_{rde_reqc}进行同步.

构件RDE求精后的结果如图 4所示.

图 4

Fig. 4

Fig. 4 Refinement in component RDE 图 4 RDE构件求精

外部应用关联构件(OAP)通过端口P_{oap_req}接收来自构件RDI的外部需求信息.

物理环境是动态变化的,当物理环境发生变化时,会使物联网内的相关物理应用进行交互以满足用户的需求.我们通过分解物理环境变化时相关联的物理应用与物理空间之间的交互过程,实现对构件OAP的精化.精化后的外部应用关联构件(OAP)内部包括3个子构件:外部应用登记子构件(PR)、外部应用分解子构件(PD)以及接收外部需求子构件(OA).这3个子构件分别对应OAP的3个端口所提供的功能.

PD要实现如下的功能:接收构件OAP的端口P_{oap_req} 传送的外部需求信息,提取需求信息中的物理位置信息;分解外部需求的物理位置信息,使分解后的每个物理位置都在相应的外部应用的物理位置范围内;根据分解后的物理位置信息,分解接收到的需求信息;发送分解后的物理位置信息以及与之对应的需求信息.用CSP将PD要实现的功能抽象为如下的事件:事件recv_oreq表示接收构件OAP的端口P_{oap_req}传送的外部需求信息,事件ext_phy表示提取外部需求信息中的物理位置信息,事件phy_preq表示分解外部需求的物理位置和与之对应的需求信息并发送给子构件PR.用CSP将子构件PD的行为表示为

PPD=recv_oreq→ext_phy→phy_preq→PPD.

PR要实现如下的功能:接收子构件PD分解后的需求信息;判断外部物理应用的物理位置是否有更新,并更新有变化的物理位置;将与外部应用相关的需求信息发送给对应的外部应用.用CSP将PR要实现的功能抽象为如下的事件:事件phy_preq表示接收分解后的物理位置信息以及与外部应用相关的需求信息,事件upd_phy表示更新外部物理应用的物理位置,事件send_oreq表示将需求信息发送给构件OAP相应的端口P_{oap_app}去实现.用CSP将子构件PR的行为表示为

PPR=phy_preq→upd_phy→send_oreq→PPR.

OA要实现如下的功能:接收外部应用发送的需求信息,并将外部应用发送的需求信息转发给RDE构件去处理.用CSP将OA要实现的功能抽象为如下的事件:事件recv_oareq表示接收外部其他应用的需求信息,事件send_oareq表示将外部应用发送的需求信息通过端口P_{oa_oap}发送给构件RDE去处理.用CSP将子构件OA的行为表示为

POA=recv_oareq→send_oareq→POA.

进程PPD与进程PPR在执行事件phy_preq时要进行同步,同步的端口分别为p15和p16.进程PPD在执行事件recv_oreq时,通过端口p17和构件OAP的端口P_{oap_req}进行同步.进程PPR在执行事件send_oreq时,通过端口p18和构件OAP的端口P_{oap_app}进行同步.OA子构件通过端口P_{oa_oap}与构件RDE的端口P_{oa_rde}进行同步.

图 5

Fig. 5

Fig. 5 Refinement in component OAP 图 5 OAP构件求精

构件OAP求精后的结果如图 5所示. 3.4 感知构件的求精

感知构件(SEN)通过端口P_{sen_req}接收来自构件RDE的感知需求信息,通过端口P_{sen_phy}从物理模型中获取感知数据,通过端口P_{sen_pro}向处理构件(PRO)发送感知处理信息.

由于物联网中的感知资源具有资源受限的特征,因此构件SEN在处理感知请求时,需要同时管理感知资源.我们通过分解感知资源的管理逻辑和感知请求的处理过程来实现对构件SEN的精化.精化后的感知构件(SEN)内部包括两个子构件:感知资源管理子构件(SRM)和感知资源子构件(SR).这两个子构件分别对应SEN的3个端口所提供的功能.

SRM要实现如下的功能:接收构件SEN的端口P_{sen_req}传送的感知需求信息,根据感知需求信息与感知资源之间的对应关系,得到实现感知需求的物理资源需求信息;根据子构件SR内感知资源的动态变化,动态更新子构件SRM.用CSP将SRM中要实现的功能抽象为如下的事件:事件recv_datareq表示接收构件SEN的端口P_{sen_req}传送的感知需求信息,事件sr_preq表示获取与感知需求对应的物理资源需求,事件upd_sr表示动态更新感知资源管理子构件.用CSP将子构件SRM的行为表示为

PSRM =recv_datareq→sr_preq→upd_sr→PSRM.

SR要实现如下的功能:接收子构件SRM发送的感知资源需求,动态更新感知资源的变化,根据感知资源需求接收从构件SEN的端口P_{sen_phy}传送的感知数据,将感知数据发送给构件PRO去处理.用CSP将SR要实现的功能抽象为如下的事件:事件sr_preq表示接收物理资源需求,事件upd_sr表示更新物理资源,事件sense_data表示接收构件SEN的端口P_{sen_phy}从物理模型中采集的感知数据,事件send_data表示将采集到的感知数据发送给构件SEN的端口P_{sen_pro}.用CSP将子构件SR的行为表示为

PSR=sr_preq→upd_sr→sense_data→send_data→PSR.

进程PSRM与进程PSR在执行事件sr_preq和upd_sr时要进行同步,同步的端口分别为p19和p20.进程PSRM在执行事件recv_datareq时,通过端口p21和构件SEN的端口P_{sen_req}进行同步.进程PSR在执行事件sense_data时,通过端口p22和构件SEN的端口P_{sen_phy}进行同步.进程PSR在执行事件send_data时,通过端口p23和构件SEN的端口P_{sen_pro}进行同步.

构件SEN求精后的结果如图 6所示.

图 6

Fig. 6

Fig. 6 Refinement in component SEN图 6 SEN构件求精

物理数据处理构件(PRO)通过端口P_{pro_data}接收来自构件SEN的感知数据,通过端口P_{pro_exe}向执行构件(EXE)发送感知处理信息.

物理应用所要处理的感知数据具有异构性,因此在对感知数据进行处理和分析之前,需要选择合适的规则对感知数据性进行预处理.我们通过分解构件PRO完成对感知数据的预处理和处理过程,实现对构件PRO的精化.精化后的物理数据处理构件(PRO)内部包括两个子构件:预处理子构件(DP)和处理子构件(DI).这两个子构件分别对应PRO的两个端口所提供的功能.

DP要实现如下的功能:接收构件SEN发送的感知数据;动态更新数据预处理规则;选择与感知数据相关的规则;根据这些规则去除感知数据中不符合逻辑、具有明显错误以及不满足用户要求等条件的“脏”数据,得到符合处理规则的数据.用CSP将DP要实现的功能抽象为如下的事件:事件recv_data表示接收构件PRO的端口P_{pro_data}传送的感知数据,事件upd_rul表示动态更新预处理规则,事件sel_rul表示选择与感知数据相关的预处理规则,pre_data表示获取经过预处理后的感知数据.用CSP将子构件DP的行为表示为

PDP=recv_data→upd_rul→sel_rul→pre_data→PDP.

DI要实现如下的功能:接收预处理后的感知数据,更新与感知数据相关的感知处理程序;根据感知数据的类型,选择合适的感知处理程序;将处理后的感知信息发送给构件PRO的端口P_{pro_exe}.用CSP将DI要实现的功能抽象为如下的事件:事件pre_data表示接收预处理后的感知数据,事件upd_pro表示更新与感知数据相关的感知处理程序,事件sel_pro表示选择合适的感知数据处理程序,事件send_info表示将处理后获得的感知信息发送给物理数据处理构件PRO的端口P_{pro_exe}.用CSP将子构件DI的行为表示为

PDI=pre_data→upd_pro→sel_pro→send_info→PDI.

进程PDP与进程PDI在执行事件pre_data时要进行同步,同步的端口分别为p24和p25.进程PDP在执行事件recv_data时,通过端口p26和构件PRO的端口P_{pro_data}进行同步.进程PDI在执行事件send_info时, 通过端口p27和构件PRO的端口P_{pro_exe}进行同步.

构件PRO求精后的结果如图 7所示.

图 7

Fig. 7

Fig. 7 Refinement in component PRO图 7 PRO构件求精

决策执行构件(EXE)通过端口P_{exe_rde}接收来自构件RDE的控制需求信息,通过端口P_{exe_pro}接收物理数据处理构件(PRO)发送感知处理信息,通过端口P_{exe_phy}向物理模型发送决策执行信息.

对物理环境所要执行的操作是根据感知处理信息和控制需求信息以及由应用行业特征生成的执行规则库决定的.我们通过分解执行操作的决定过程,实现对构件EXE的精化.精化后的决策执行构件(EXE)内部包括子构件:决策子构件(ST).这个子构件对应EXE的3个端口所提供的功能.

ST要实现如下的功能:接收构件EXE的端口P_{exe_rde}传送的控制需求信息,获取控制类型、控制数据等与控制相关的参数;接收构件EXE的端口P_{exe_pro}传送的感知处理信息,获取感知类型、感知信息值等与感知相关的参数;更新子构件ST内的用来生成决策执行信息的执行规则库;根据控制信息与感知信息来选择应该执行的规则;根据选择的规则,控制需求信息和感知处理信息来生成决策执行命令,并将决策执行命令传送给构件EXE的端口P_{exe_phy}.用CSP将ST要实现的功能抽象为如下的事件:事件recv_conreq表示接收EXE的端口P_{exe_rde}传送的执行需求信息,事件recv_info表示接收EXE的端口P_{exe_pro}传送的感知处理信息,事件upd_lib表示更新执行规则库,事件sel_esr表示根据执行需求和感知信息来选择执行规则,事件send_coninfo表示传送决策执行命令给构件EXE的P_{exe_phy}端口.用CSP将子构件ST的行为表示为

PST=recv_conreq→recv_info→upd_lib→sel_ser→send_coninfo→PST.

进程PST在执行事件recv_conreq时,通过端口p28和构件EXE的端口P_{exe_rde}进行同步.进程PST在执行事件recv_info时,通过端口p29和构件EXE的端口P_{exe_pro}进行同步.进程PST在执行事件send_coninfo时,通过端口p30和构件EXE的端口P_{exe_phy}进行同步.

构件EXE求精后的结果如图 8所示.

图 8

Fig. 8

Fig. 8 Refinement in component EXE图 8 EXE构件求精

为了验证R-SEM是否保持了原模型所具有的性质——不死锁、不中止和不发散,我们进行了以下两部分内容的验证:(1) 每个构件内部的子构件之间的交互保持原有模型的性质;(2) 子构件的端口与构件端口之间进行的同步保持原模型的性质.下面以R-SEM内的需求判别构件RDI为例,说明验证的过程.

首先,对构件RDI进行第1部分的验证.构件RDI内部有3个子进程PRR,PLR和PER;存在着两个交互:PRR和PLR之间的交互以及PRR和PER之间的交互,分别用进程PR_LR和进程PR_ER表示.相应的验证代码如下所示:

· PRR=recv_ereq→laddr→ext_paddr→comp_addr→lreq→exreq→PRR;

· PLR=laddr→lreq→send_inreq→PLR;

· PER=exreq→send_oreq→PER;

· PR_LR=PRR||PLR;

· PR_ER=PRR||PER.

用模型检验工具PAT验证交互进程是否满足不死锁、不中止和不发散的性质,相关的验证语句在PAT中可表示为

· #assert PR_LR deadlockfree;

· #assert PR_LR divergencefree;

· #assert PR_LR nonterminating;

· #assert PR_ER deadlockfree;

· #assert PR_ER divergencefree;

· #assert PR_ER nonterminating.

验证结果如图 9所示.从图 9可以看出,构件RDI的内部交互是保持感执模型的原有性质的.

图 9

Fig. 9

Fig. 9 Result of verification about interaction inside the component RDI图 9 构件RDI的内部交互验证结果

其次,对构件RDI进行第2部分的验证.子构件RR通过端口p5与构件RDI的端口P_rdi-req进行同步,子构件LR通过端口p6与构件RDI在端口P_{rdi_ireq}进行同步,子构件ER通过端口p7与构件RDI在端口P_{rdi_oreq}进行同步.子构件的端口与构件的端口之间具有输入/输出的同步关系,假设子构件的端口上运行着进程P,构件的端口上运行着进程Q,则对RDI的第2部分的验证等价于验证具有导管连接的进程P和进程Q是否满足感执模型的性质.P和Q通过导管连接,可用CSP表达为R=P》Q.因为进程P和进程Q都不死锁和不中止,因此,进程R也不死锁和不中止.由于P和Q都与其他构件的进程或构件内部的进程有连接,因此,P和Q进行导管运算后也不会发散,即进程R不会发散的.因此,构件RDI内部的端口与构件RDI的端口之间的同步也满足感执模型的 性质.

因此,构件RDI保持了感执模型原有的性质.

同样地,可以通过上述方法对构件RDE、构件OAP、构件SEN、构件PRO和构件EXE进行分析.分析结果表明,这5个构件都能保持感执模型原有的性质.

综上所述,感执模型经过精化后,仍然保持原有的性质.也就是说,基于求精后的感执模型设计的物理应用以及物理应用互联构成的物联网软件满足不死锁、不中止和不发散的性质.这将为物理应用的设计以及物联网软件的设计提供有效的指导.

本文在基于物理模型的物联网软件体系结构(PMDA)研究的基础上,根据物联网软件设计的需求,实现了对SEM求精的模型R-SEM.R-SEM考虑了物联网的特有属性,将SEM的内部构件按照物理应用的感执工作流程分解为用通信顺序进程(CSP)表达的子构件来说明构件端口的功能的实现,并用CSP中的运算符导管说明子构件的端口与构件端口是如何同步的.采用CSP对子构件之间的交互进行了描述,并验证了精化后的感执模型保持了原模型所具有的保证物理应用之间有效互联的性质:不死锁、不中止和不发散.由于R-SEM精化了SEM的内部组成,且保持了SEM的有效互联性质,因此,R-SEM对最终将PMDA应用于物联网软件开发具有实际的指导意义.

下一步的工作是将PMDA中的其他两个模型进行精化,使得PMDA更加明确物联网在用户需求以及物理实体方面所需要实现的功能,并基于精化后的软件体系结构开发实际的物联网软件系统.