论文研究-分布式制造调度体系结构的π演算形式化建模.pdf

所需积分/C币:9 2019-09-07 13:24:01 693KB .PDF
34
收藏 收藏
举报

分布式制造调度控制体系结构的良好形式化设计是确保后续开发系统一致性和高效性的基础。以Agent(Holon)的制造调度控制体系结构模型为对象,在比较现有形式化方法优劣的基础上,提出基于一阶多元π-演算的体系结构形式化建模和分析方法,并以一种基于Holon的柔性制造车间生产调度控制体系结构为实例,重点对各个实体的通信协调机制进行了形式化分析,并借助计算机工具进行了相应的死锁分析。结果表明了基于一阶多元π-演算在形式化建模和分析方面的有效性。
王世进:分布式制造调度体系结构的丌演算形式化建模 2010,46(9)3 模型为基础,设计表1所列的 Holon之间的消息链接,以定义 aResch, aResch7, aResch},71和72分别指单元内的自治调 链接的输出端口、输入端口和传递的消息。并假设链接是一对度和重调度计算过程,属于单元内部行为,其他 Holon不可见。 的,如仅有vps链接可用于PH-to-SH,仅有s链接可用于3.5形式化分析 SH-o-CH。表中所有链接都以“w”或“v”为首,所有的消息均以 作为一种强大和成熟的形式化方法,π演算有支持其正确 “x”或“y”为首 性验证和相关应用的工具,如JACK工具集、基于丌演算的语言 表1 Holon之间的消息链接 PICT、可执行的π演算EP以及传值进程代数工具VPAM叫。 名字发送者接收者消息类型 采用基于 New Jersey SML语言编译器的MWB( Mobility SH 请求分配( rEap) Workbench)ta(http://www.it.uu.se/research/group/mobility/mwb) (1)请求路径分配决策( tRees) MWB工具是用于操作和分析并发系统的自动化丌演算工具 WSO SH CH (2)路径分配(yAs) 能用来分析进程的一些基本错误:如类型错误、缺少同步等,并 (1)响应请求( cRespo) 具有基本推理功能,包括死锁分析( deadlocks命令)、行为相似 (2)通知调度结果( sEres) 性(eq命令)交互模拟跟踪(step命令)等。着重对各个 Holon (3)拒绝( rEfuse) (1)通知路径分配(xAss) 和整体系统进行了初步的死锁分析。 (2)拒绝( rEfuse) 为将π演算输入MWB,需将通常的π演算做一些转换。 CH 建立分配关系( rrela) 根据如表2所示的转换规则,上述的各个 Holon可以描述成 (1)进行调度( t SchR) MWB理解的公式。如资源 Holon描述为 wCI CH RH (2)进行重调度( aResch) agent RH(ucr, urc, xSchR, xRegrs, yReschR)= (1)进行调度( t Schet TH wcr(xSchR)RH(wcr, vrc, xSchR, xRegrs, yReschR )+ (2)进行重调度( bRecht) pCHP通知调度结果 esche) .urc<xRegrs>wcr(yReschR)RH(wcr, urc, xSchR RHCH请求重调度( dEgre) xRegrs, yReschR)) (8) vro PH TH 建立层次关联( rrela) 然后,将所有MWB公式放到一起以“ HFMSag”为文件名存盘。 表2MWB与π演算转换的映射 34形式化描述 MWB 丌演算 含义 结合消息链接和图2的消息传递模型,形式化模型简化 约束算子 如下: 抽象 零进程 HMS=PH(…)SH(…)CH(…)RH(…)TH(…) 输出 PH(c)=wps<xRegp>(xTOut PH(c)+usp(msg) 内部活动 α( nist).a.(Ⅶ nist)输入前缀 ([msgexAss] upc<xRela> upt<rEla> a< nist>a.[nlis输出前缀 ucp(xschre PH(c))+msg=xRefuse] PH(c)))(3) ItH, c=ups, usp, wpc, wpt,vcP, xReqp, xTOut, xAs.,rEla,xschre 注: nist为一非空名字列表 rEfuse}, x TOut表示等待超时。 设置分析测试环境为: Standard ML of New Jersey100.7, MwB’99 version4.135和 Windows操作环境。图3为初步死锁 SH(sc)=ups(xReyp)wse<xReqs>(xTOuls SH(sc)+ 分析结果,表明整个体系结构模型内不存在死锁( No deadlocks vcs(msg)([msg=xRespc] Tswsc<yA ss>.USP<xAss> found),这为将来构建可靠的系统和进行合理的调度控制活动 vcs(yScres )SH(sc))+(msg=xRefuse] SH(sc))(4) 打下了良好基础。 IH,Sc=ups, wsc, vcs, usp, xReqp, xReqs, xTOuts, xRespc, yA.s xAss, aCres, rEfuse},rs指SH内部评价投标的计算过程。 he Mobi1主 y Workbench built Thu Jan 08 13:13:4L 2004) RH(rc)=wcr(xSchR) RH(rc)+ CUpa, uac, Ucs, uap, Reqp, xReqs, xT Outa, xReapr yAas, xAas, yScres, xRef arrc<xRegrs> wcr(yReschR) RH(rc) uap wpc. upt. uc p. xRerm. xTOutp xAap xRe la. xachre. xRe fuse) pe. xTOutc, yA=s. xHe la. xSch Screa. xachre. xRegrs. xRep-e. vReschR. Reacht rEach> 其中,rc={vcr,utr,vre, sChr, rEars, yReschr},Tr指机床故障 No deadlocks found. 等资源内部动作或事件。 pt, uct, xRe la, xScheT, yReschI) a numher N g to se legt the NEh conmitrunt TH(t)=pt( rEla)·(t( x Sche t)·TH(te)+ hR》·t," vnC<xReg"8 uct(yReschT) TH(tc)) g:1)vrc. LxReurs Iwcr(yReschR6.RH<wcr, vrc, xBchR xRegrs, yReschR6> 其中,tc={vpt,vct, rela, x Schet, aResch们}。 图3MWB死锁分析界面 CH(cc)=wsc(xRegs)T1vcs<xRespc>(xTOutc CH(cc)+ sc(yAss)·upc( rRela)·vcr< SchR> 4结束语 uct<xSche T>vcs<yScres>ucp<xschre>CH(cc))+ 从软件体系结构的观点出发,探讨了基于一阶多元π演算 (rc( rEars)+sc( dEgre)·r2:wcr< aResch>的体系结构的形式化描述和分析。并以一基于 Holon的柔性制 ucty ReschT>vcs<yReschs>CH(cc) (7)造车间生产调度控制体系结构模型为实例,详细描述了该模型 其中,ce={use,wres,wpe,wcr,wct,cp,re,κReqs, cRespo, rOUte,实体的通信和协商关系之间的丌演算,并借助计算机工具进行 yAss, xRela, sChr, x Schet, ysc res schre rEars, xRegre (下转7页)

...展开详情
试读 3P 论文研究-分布式制造调度体系结构的π演算形式化建模.pdf
立即下载
限时抽奖 低至0.43元/次
身份认证后 购VIP低至7折
一个资源只可评论一次,评论内容不能少于5个字
您会向同学/朋友/同事推荐我们的CSDN下载吗?
谢谢参与!您的真实评价是我们改进的动力~
  • 至尊王者

关注 私信
上传资源赚钱or赚积分
最新推荐
论文研究-分布式制造调度体系结构的π演算形式化建模.pdf 9积分/C币 立即下载
1/3
论文研究-分布式制造调度体系结构的π演算形式化建模.pdf第1页

试读结束, 可继续阅读

9积分/C币 立即下载