（控制理论与控制工程专业论文）基于pi演算的无线自动售货机系统建模与应用.pdf

大连理工大学硕士学位论文 摘要 无线自动售货机系统通过无线网络实现了对自动售货机的远程监视和控制，便于企 业内部物流管理及向顾客提供方便的手机购物。为了对这一复杂系统形成一致的理解， 分析系统的正确性和可靠性，进而定量评估系统的绩效，需要建立一种严谨的可模拟系 统动态运行的模型。 由于无线自动售货机系统属于离散动态系统，本文采用了描述分布式并发系统的 p i 演算过程代数方法为系统建模。分别对系统的交易流程和物流配送过程建立了p i 演 算模型。对无线自动售货机系统的交易流程的建模采用自顶向下的建模方法，首先建立 系统的主要活动模块的顶层p i 演算模型，然后对这些模块进行细化，最后得出系统交 易流程完整的p i 演算模型；并用p i 演算的形式化辅助工具m w b 验证其正确性。为了 能够对无线自动售货机系统物流配送过程进行建模，本文定义了一种带时间因素的p i 演算，对无线自动售货机系统的物流配送过程建立了含有时间因素的p i 演算模型；考 虑到绩效分析的需要，还在不同的缺货情况下同时模拟两种系统物流配送过程的运行， 通过选择最佳的配送路线，得出无线售货机物流配送过程与传统售货机物流配送过程工 作效率的提高。 本文为系统复杂的交易流程和物流配送过程建立了精确的p i 演算模型，使系统的 开发人员、监控人员和维护人员对系统形成了一致的准确的理解，为系统的分析和改进 打下良好基础。同时对系统物流配送过程进行量化，实现了无线自动售货机系统的时间 绩效分析。 关键词：无线自动售货机系统；p i - 演算；系统建模；绩效分析 m o d e l i n ga n da p p l i c a t i o no f w i r e l e s sv e n d i n gm a c h i n es y s t e m b a s e do np i c a l c u l u s a b s tr a c t w i r e l e s sv e n d i n gm a c h i n es y s t e mr e a l i z e st h el o n g - d i s t a n c ec o n t r o l ，i ti sc o n v e n i e n tf o r e n t e r p r i s et om a n a g et h ed i s t r i b u t i o n ，a l s oe a s yt ob es h o p p i n gb yp h o n ef o rc u s t o m e m t o r e a c ha l la g r e e m e n to nt h ec o m p l i c a t e ds y s t e mu n a n i m o u s l y , a n a l y z er e l i a b i l i t y a n dt h e e f f i c i e n c ya m e l i o r a t i o no fw i r e l e s ss y s t e m ，f i n d i n ga na c c u r a t em o d e lt h a t c a l lm o d e lt h e s y s t e md y n a m i c a l l yi san e c e s s a r y w i r e l e s sv e n d i n gm a c h i n es y s t e mb e l o n g st ot h ed i s c r c t ee v e n td y n a m i cs y s t e m ， p i c a l c u l u sw h i c hi sak i n do ft h ep r o c e s sa l g e b r ac a l la n a l y z ea n dm o d e lt h es y s t e mt h a th a s c h a r a c t e r i s t i c sa sc o n c u r r e n ta n dr e s o u r c es h a r i n gu s e f u l l y p i c a l c u l u sm o d e l i n gt e c h n o l o g y i sa p p l i e dt om o d e la n dr e s e a r c ht h ew i r e l e s sv e n d i n gm a c h i n es y s t e mt om o d e lt h eb u s i n e s s p r o c e s sa n dt h el o g i s t i c sd i s t r i b u t i o np r o c e s s t h em o d e l i n gm e t h o dc a l l e d “f r o mt o pt o b c i t t o m ”i st om o d e lb u s i n e s sp r o c e s s t h et o pp i - c a l c u l u sm o d e li sb u i l ta i m i n ga tt h em a i n a c t i v i t i e sm o d u l e so ft h es y s t e m a n dt h e nt h ei n t e g r a t e dp i - c a l c u l u sm o d e lo fb u s i n e s s p r o c e s si sf o u n d ，a to n et i m e ，t h r o u g he x e c u t i n g o nt h es i m u l a t o rm w bt op r o v et h ec h a n g e d s t n l c t u r eo ft h es e e at i m e dp i c a l c u l u sm o d e lw i t ht i m ei sd e f i n e dt om o d e lt h el o g i s t i c s d i s t r i b u t i o np r o c e s so ft h ew i r e l e s ss y s t e mi nad e f i n i t ed i s t r i b u t i o ne n v i r o n m e n t c o n s i d e r e d t h en e e do fp e r f o r m a n c ea n a l y s i s ，t h em o d e lo ft h e | o g i s t i e sd i s t r i b u t i o np r o c e s so ft h e t r a d i t i o n a lv e n d i n gm a c h i n es y s t e mi sf o u n dt o o t h e s et w om o d e l sa r es i m u l a t e di nd i f f e r e n t s i t u a t i o n s i n 血i sp a p e ra na c c u r a t ep i c a l c u l u sm o d e li s b u i l tf o rt h eb u s i n e s sp r o c e s so ft h e s y s t e m ，c a nm a k et h ep e r s o n n e lo ft h es y s t e mt of o r ma u n i f o r ma n de ：礤a c tc o m p r e h e n da n d g r o u n daw e l lf o u n d a t i o nf o rt h ea n a l y s i sa n di m p r o v e m e n to ft h es y s t 劬t h em o d e l i n gf o r t h el o g i s t i c sd i s t r i b u t i o np r o c e s so ft h ew i r e l e s ss y s t e mq u a n t i f i e st h ee f f i c i e n c ya m e l i o r a t i o n o fw i r e l e s ss y s t e ma n dr e a l i z e st h et i m ep e r f o r m a n c ea n a l y s i so ft h ew i r e l e s sv e n d i n g m a c h i n es y s t e m k e yw o r d s ：w i r e l e s sv e n d i n gm a c h i n e p e r f o r m a n c ea n a l y s i s s y s t e m ；p i - c a l c u l u s ；s y s t e mm o d e l i n g ； 一i i 大连理工大学硕士研究生学位论文 大连理工大学学位论文版权使用授权书 本人完全了解学校有关学位论文知识产权的规定，在校攻读学位期间 论文工作的知识产权属于大连理工大学，允许论文被查阅和借阅。学校有 权保留论文并向国家有关部门或机构送交论文的复印件和电子版，可以将 本学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、 缩印、或扫描等复制手段保存和汇编本学位论文。 学位论文题目： 豆ae i 二2 量粤刍刍越蕴垒壶壶亟笪拉丞f 超撞量睦图 导师签名：星窒亟 大连理工大学学位论文独创性声明 作者郑重声明：所呈交的学位论文，是本人在导师的指导下进行研究 工作所取得的成果。尽我所知，除文中已经注明引用内容和致谢的地方外， 本论文不包含其他个人或集体已经发表的研究成果，也不包含其他已申请 学位或其他用途使用过的成果。与我一同工作的同志对本研究所做的贡献 均已在论文中做了明确的说明并表示了谢意。 若有不实之处，本人愿意承担相关法律责任。 学位论文题目：盘互2 曼二2 蹙翼坠丑盛皂迎焦堡赴叁5 赴莲熔墨i 些圆 作者签名： 王函趣 日期：垒塑堡年盟月j 丝日 大连理工大学硕士学位论文 1绪论 1 1 课题的研究背景和意义 随着无线信息技术的快速发展，信息可以在任何时间、任何地点传递。移动商务以 新的信息传递和处理方式在市场中涌现出来，成为企业丰富产品和服务、提高商务活动 绩效的有力手段。其中无线自动售货机系统成为无线信息技术与传统商务结合的典型移 动商务应用实例，逐渐在市场上出现。在传统的自动售货机上嵌入无线通信模块后，不 仅能远程控制售货机出货，而且能及时采集销售信息，方便后台管理。本文研究背景源 于某公司基于u s s d 平台开发的无线自动售货机系统【1 1 。该系统利用中国移动g s m 网 络作为通信的载体，既实现了向顾客提供新颖的手机话费支付或“积分 换商品服务， 又改进了企业内部的物流配送管理。 无线自动售货机系统不仅给企业提供了新的机遇，也提出了新的挑战。由于无线信 息技术的引入，为企业信息管理带来了新的问题，系统分析和设计的复杂性增加。关注 传统商务和电子商务之间的物理和虚拟存在形式不同，c h o i 2 】研究电子商务市场，提出 “主体”、“产品 和“流程是电子商务市场领域的三个要素。移动商务是电子商务 的扩展，作为一种新的移动商务模式，无线自动售货机系统涵盖了移动商务的基本特性 和核心功能，并突破了移动服务领域只限于非实物型信息商品服务的限制。同时利用移 动商务的空间移动优势，把传统有线网络的实物交易服务引入到移动业务中，实现了在 任何时间、任何地点的信息传送，是信息技术在空间和时间效率方面的进一步提升。因 此，无线自动售货机系统也包含移动商务的三个组成要素 2 1 ：产品( 货物) 、业务流程( 交 易过程、物流配送管理) 和主体( 手机、自动售货机) 。其中业务过程联系着产品和主体， 对业务过程的研究对于移动商务有着重要的意义。因此，怎样为该系统的业务过程进行 建模，能否对过程绩效指标进行定量的分析和计算，能否以此为基础，设计和实现实用 的信息系统等问题的提出，需要寻找合适的建模方法。 目前，移动商务系统多采用表意的图形化表达，其缺点在于模型不够精确，导致系 统开发人员、监控人员和维护人员对系统的理解不一致。同时这种图形化表达不便于动 态模拟系统的运行情况，不利于检查系统中存在的设计缺陷。以往对无线自动售货机系 统的研究也多集中在定性的技术层面上的分析，缺少定量的描述，不便于系统的绩效分 析。 无线自动售货机系统属于离散事件动态系统，其特点在于系统中的状态演化是由事 件驱动的，即在驱动事件发生的瞬时，状态才能出现跃变；系统的状态变化具有异步性、 基于p i 填算的无线自动售货机系统建模与应用 并发性和不确定性；系统服从的是人为的逻辑规则，导致通常不能采用传统的微分方程 或差分方程来描述。 p i 演算是一种形式化语言，常用于描述具有移动性、并行性、并发性、交互性的离 散事件动态系统。p i 演算是以进程间的移动通信为研究重点的并发理论，是对过程代数 c c s ( c a l c u l u so fc o m m u n i c a t i o ns y s t e m ) 的扩展，不但可以传递c c s 中的变量和值，而 且还可以传递通道名，使其具有建立新通道的能力，因此p i 演算常用来描述结构不断 变化的并发系统。p i 演算是描述移动过程的专门技术，支持对动态检测，并提供很多工 具以支持正确性检测及其相关工具集、基于p i 演算的语言p i c r 、可执行的p i 演算代数 工具v p a m 等。围绕p i 演算有很多研究工作已经展开，大致可以分为两方面：( 1 ) p i 演算本身的理论研究，如p i 演算的互模拟等价性、类型系统以及p i 演算的有穷公理化 问题【3 ，4 】；( 2 ) p i 演算作为建模工具在计算机软件系统各个研究方向上的应用，如人工智 能、分布式组件技术【5 ，6 1 等。用p i 演算对无线自动售货机系统建立一种精确的可模拟系 统动态运行的模型，可以使系统的开发人员、监控人员和维护人员对系统达成一致的准 确的理解。通过用代数、形式语言、自动机的方法来定性或定量的分析p i 演算模型的 一系列性质，还可以为系统的设计和改进打下良好的基础。同时还可以在p i 演算模型 中加入时间概念，对系统建立含有时间因素的模型，定量地分析无线系统的效率改进， 从而实现对无线自动售货机系统的绩效分析。 基于p i 演算的无线自动售货机系统的建模方法，可以指导系统的开发、优化信息 过程、使信息系统更实用，从而帮助企业实现移动状态信息化，提高效益和工作效率。 1 2 国内外研究概况及发展趋势 1 2 1 无线自动售货机的发展和研究现状 世界上最早的自动售货机出现在公元前3 世纪，那是埃及神殿里投币式圣水出售机。 1 7 世纪，英国的小酒吧早设有了香烟的自动售货机。自动售货机的真正普及是在第二次 世界大战以后。2 0 世纪5 0 年代“喷水型果汁自动售货机 大受欢迎，果汁被注入到纸 杯里出售。到了8 0 年代，自动售货机在美国和日本被广泛使用，后逐渐散布世界各地， 主要是发达国家。二十多年间，自动售货机队伍逐渐发展壮大，尤其是在日美等地见 自动售货机是2 0 世纪9 0 年代开始试探着进入中国的，但由于刚走上街头不久的自动售 货机都被人为破坏，所以自动售货机的发展在中国一时停滞不前。随着时间的推移和传 媒的不断宣传，消费者开始认知并接受，行业的发展趋势一点点地好转起来。许多业内 人士认为自动售货机在中国也会像美国、日本一样掀起一场零售业的变革。 大连理工大学硕士学位论文 近几年，移动商务的快速发展使无线自动售货机走上了历史舞台。无线自动售货机 继承了自动售货机所有的优点，更提供了一种方便的交易支付方式一手机话费支付， 使用户可以不用支付现金就能够购买商品i s j 。在中国，无线自动售货机正在逐渐普及， 重庆、成都、北京、上海、香港、辽宁和吉林的大部分城市都有了一定规模的应用，而 且都取得了一定的经济效益。 目前国内外关于无线自动售货机的研究主要集中在对其基本结构和实现原理等技 术层面定性的介绍和分析。文献【1 0 】介绍了将短信息应用嵌入自动售货机支付系统的原 理及其硬件电路和软件设计。文献1 1 1 阐述了以移动增值服务为基础的手机自动售货机 的嵌入式系统设计。文献【1 2 】介绍了一种基于网络的自动售货机的实现方法。文献 1 3 】 设计了一种基于移动支付的自动售货机结构，并给出总线转换接口的软硬件实现思路。 但关于无线自动售货机系统的建模分析的研究文献却很少。近几年出现了p e t r i 网对无 线自动售货机系统的建模与应用研究【1 4 1 ，但p e t r i 网建模并发系统时存在缺陷，限制了 p e t r i 网理论在离散事件动态系统领域的发展。p i 演算是分布式并行系统的建模和分析 工具，常用于描述具有移动性、并行性、并发性、交互性的离散事件动态系统。它以其 特有的优势在建模离散事件动态系统时可对系统建立准确的可模拟系统运行的模型，并 通过对系统进行定量的分析更加能够说明无线移动技术引进给自动售货机系统带来的 改进。 1 2 2p 卜演算建模理论的发展和研究现状 计算模型一直是计算机科学研究的重要问题。a 演算是顺序计算的经典模型。而p i 演算是二十世纪九十年代计算机并行理论领域最重要的并发计算模型，它能够描述结构 不断变化的并发系统，它由m i l n e r 、p a r r o w 和w a l k e 在e n g b e r g 和n i e l s e n 工作的基础 上，对c c s 进行扩充而得到的。 从一开始，并发理论的研究就集中在并发系统的形式模型和形式语义上。其结果是 从不同侧面反映并发本质的各种模型被相继提出：从六十年代的p e t r i 网到七、八十年 代的c s p 、c c s 和传值c c s ( v a l u e p a s s i n gc c s ) ，再到九十年代的p i 演算等，尽管它 们回答的是同一问题，即“什么是并发 ，但各种模型间的差异是明显的，表现在是采 用真并发还是交错式语义，理论是基于代数方法、图形表示还是逻辑方法等方面1 1 5 】。 p e t r i 网是用来描述并发异步活动的系统模型，用于提供一种形式化的表示顺序、并 发概念以及标识和解决歧义性的方法。它是规范和验证通讯协议的一种有效工具。该模 型虽然能够用于精确的说明顺序、并发和同步等概念并能够很好地定义和解决并发系统 中很多性质，如正确性、无死锁性、互斥等，但用于描述并发系统时存在两个缺陷： 一3 一 基于阼演算的无线自动售货机系统建模与应用 ( a ) 首先，它在本质上只有一层，并不具有层次结构； ( b ) 其次，它只能说明系统的控制流而不能说明系统的数据流，即使网转换条件由 数据值来表示，改变和存储数据变量值的语义仍不属于p e t r i 网的一部分【1 6 1 。 进程代数是一种形式化描述复杂并发系统的建模工具，是一种高层的描述语言，是 支持并发分布系统的组合描述及其性质形式化证明的代数语言。它以代数形式来描述模 型，并为模型化的系统定义了一套完整的语法和语义【1 7 1 。进程代数有很多种，其中主要 的有b e r g s t r a 和k l o p 的a c p ( a l g e b r ao fc o m m u n i c a t i n gl r o c s s e s ) 【埘，h o a r e 的 c s p ( c o m m u n i c a t i o ns e q u e n t i a lp r o c e s s e s ) t 1 叭，m i l n e r 的c c s ( c a l c u l u so fc o m m u n i c a t i n g s y s t e m s ) 2 0 j 乖! i s o 的l o t o s ( l a n g u a g eo ft e m p r o r a lo r d e r i n gs p e c i f i c a t i o n s ) 2 1 】等。这些 进程代数可以通过附加时间( 时间进程代数( t i m e dp r o c e s sa l g e b r a ) ) 或概率信息( 概率进程 代数( p r o b a b i l i s t i cp r o c e s sa l g e b r a ) ) 等指标加以扩展，使其表达力更强，可用于并发系统 的性能评价，比如p e p a ( p p e f f o r m a n c ee v a l u a t i o np r o c e s sa l g e b r a ) 等。 p i 演算是对c c s 的扩展，它是由m i l n e r 、p a r r o w 和w a l k e 在e n g b e r g 和n i e l s e n 工作的基础上提出的。它扩展了c c s 的并发计算能力。此模型忽略了c c s 中的通道和 变量的差别而将它们统一为名字，所以它的基本计算实体只有名字和进程，进程之间的 通信是通过传递名来完成的。由于可以传递通道名，因此p i 演算具有了建立新通道的 能力，所以p i 演算可以用来描述结构不断变化的并发系统f 即系统中进程之间的连接关 系可随着进程状态的不断变化而发生改变) 。与c c s 不同，它是一个封闭的计算模型。 可用于描述结构动态可变的系统。 p i 演算在经过多年的发展中不断扩展和完善，作为一种新的建模语言被广泛应用到 计算机科学的各个领域，例如线路设计、网络协议、软件工程、人工智能、形式语义、 操作系统、并行编译、数据管理等，并逐渐形成了今天系统的p i 演算理论。 p i 演算在系统建模和性能分析中的作用越来越被人们所接受，它在计算机科学领域 中的发展潜力毋庸置疑。p i 演算和移动商务两个先进计算机技术的结合也是一种必然的 趋势，不仅可以促进移动电子商务的发展，还将有助于p i 演算理论的进一步完善。 1 3 本文的研究工作和框架结构 本文将p i 演算建模技术应用于无线自动售货机系统的建模和应用研究。在深入研 究系统特点的基础上，建立实际系统的交易流程的p i 演算模型，通过仿真工具m w b 验证售货机应用服务器模型的正确性。定义了一种带时间因素p i 演算，建立实际系统 的物流配送的p i 演算模型，同时在不同的情况下模拟系统物流配送过程的运行情况， 大连理工大学硕士学位论文 与传统的自动售货机系统进行比较，将系统地效率改进进行量化，实现了对系统的时间 绩效分析。本论文各章的具体内容如下： 第一章介绍本文的研究背景和意义、无线自动售货机和p i 演算理论的发展及国内 外的研究现状。 第二章主要介绍离散事件动态系统和p i 演算的基础理论。包括离散事件动态系统 的概念、三种层次模型；p i 演算的特点、语法、操作语义、互模拟等价关系、代数公理。 第三章分析研究了无线自动售货机系统的工作原理及各组成部分的运行机理，包括 u s s d 系统平台、移动中间件系统、应用服务器。 第四章在分析系统交易流程的基础上，采用自顶向下的方法建立系统交易流程的顶 层p i 演算模型，再将主要的活动逐层细化，最终得到无线自动售货机系统交易流程的 完整的p i 一演算模型，并用p i 演算的形式化辅助工具m w b 验证售货机应用服务器模型 的正确性。 第五章定义了一种带时间因素的p i 演算，对无线自动售货机系统的物流配送过程 进行p i 演算建模及分析，同时模拟、分析和验证了两台缺货的售货机补货配送的情形， 实现了对无线自动售货机系统的时间绩效分析。 基于阼演算的无线自动售货机系统建模与应用 2 基础理论介绍 2 1 离散事件动态系统 2 1 1 离散事件动态系统的概念 离散事件动态系统( d i s c r e t ee v e n td y n a m i cs y s t e m s ，简称d e d s ) 是由国际自动控制 专家、哈佛大学何毓琦( h o ，y c ) 教授于2 0 世纪8 0 年代初提出的【捌，是一个区别于连 续变量动态系统( c o n t i n u o u sv a r i a b l ed y n a m i cs y s t e m ，简称为c v d s ) 的概念。它是指离 散事件按照一定的运动规则相互作用而导致状态演化的一类动态系统，如自动化生产 线、计算机通讯网络、交通系统、军事一i 系统等。这些系统中存在着大量的离散事件 过程，它们的演化过程不能用连续变量来描述吲，不是由物理学定律所描述的，而是服 从人为的一些复杂规则【2 4 1 。d e d s 的主要特点是：不连续性、性能测度的连续性、随机 性、层次性、动态性、知识和经验的重要性、计算的复杂性和应用的广泛性。 d e d s 研究中最基本的一个问题是系统的建模。针对这一类系统的建模方法有两大 类：非形式化建模和形式化建模。非形式化的建模技术是指借助于计算机技术，通过人 们易于接受并理解的图形表示对系统建模，然后转化为计算机语言，通过程序对系统进 行分析。主要有活动循环图法( a c d 法) 、流程图法、面向对象的建模技术等。形式化 的建模是指采用大量的数学工具通过状态方程对系统进行描述和分析，主要有排队网络 法、极大代数法、扰动分析法和p i 演算建模法等【2 5 1 。 2 1 2 离散事件动态系统的三种层次模型 在d e d s 的控制问题的研究中，对系统的建模是从不同层次和用不同数学工具来进 行的，包括逻辑层次、时间层次和统计性能层次闭。 ( 1 ) 逻辑层次：主要关心事件和状态这两个主要因素相互作用和演化的逻辑顺序关 系。这两者都是有限、离散的集合，所用的数学模型包括有限自动机和形式语言、p i 演算、有限递归过程、通讯序贯进程乃至图论、有限域代数等。它们的主要困难也是共 同的，即离散运算的组合复杂性问题。尽管在逻辑层次赋予代数结构有助于解决这一问 题，这里已有的概念和工具都是逻辑、代数或计算机专家们提供的，但有关控制的问题 则是近几年才提出的。r a m a d g e 和w o n h a m 提出的基于自动机和形式语言的监控理论是 比较完整的一种，它把现代控制理论的主要概念移植过来。这一层次的模型和方法已经 在若干实际问题中得到了应用。 大连理工大学硕士学位论文 ( 2 ) 时间层次：在逻辑层次模型中引入时间，不但可使d e d s 呈现更丰富多彩的动 态性质，而且可导致对系统性能的定量的评估。目前，在许多人的努力下可以建立一套 平行于传统线性系统的控制理论，当然它们的合理性和现实意义要靠其能说明和解决的 客观世界的问题来证实。 ( 3 ) 统计性能层次：这类模型通常也被称为随机d e d s ，需要排队网络、马氏链、 广义半马氏过程等数学框架来处理。理论上通常只在马氏过程或者具有乘积形式解时才 有可行的处理方法，应用上则发展了许多近似计算方法，以及像扰动分析这样基于仿真 的分析和静态优化方法。这一层次的理论在制造系统、通讯网络、计算机系统性能评估 等方面仍被广泛应用。特别是其独特的随机优化和随机控制问题正吸引着大量的研究工 作。 尽管这三种层次的方法研究的是同一类过程，但它们的不同的侧重点和不同的描述 手段使之组成了d e d s 的一个“模型体系，以适用于不同的研究目标。目前，基于逻 辑层次模型、时间层次模型和统计层次模型的研究d e d s 的各种方法，都已得到了很大 程度地发展，开始形成具有各自特色的理论框架。 2 2p - 演算的基本理论 p i 演算是分布式并行系统的建模和分析工具，常用于描述具有移动性、并行性、并 发性、交互性的离散事件动态系统。p i 演算是通过利用形式化语言来描述和分析离散事 件动态特性，具有良好的离散事件处理模型的能力，同时也可作为对事件的发生过程进 行模拟的工具。它是建立在严格的数学基础上的，可对模型进行分析、验证和形式化【2 7 】。 目前，p i 演算理论已发展成为一个比较完整的体系，已经成为在逻辑层次上对离散事件 动态系统进行建模和分析的主要方法之一。 2 2 1 p i - 演算的特点 p i 演算旨在成为交互并发系统的理论基础，并因此采用交互作为它的变元 ( p r i m i t i v e ) ，如同入演算采用函数应用( f u n c t i o na p p l i c a t i o n ) 作为它的基元一样。 p i 演算的基本计算实体是名字和进程，名字即为连接的名字，进程通过他们共享的 名字进行交互，而关键的要点在于进程在交互中通信的数据同样是名字，交互中接受的 名字能够用来参与其他交互。通过接受名字，进程能够动态得到与其他进程进行交互的 能力。因此，整个系统的结构，即系统构件之间的连接关系能够伴随时间任意演化【矧。 分析p i 演算对并发计算的处理方法，以下特征值得重视： ( a ) 从函数观念到交互观念的转换 基于1 , i - 演算的无线自动售货机系统建模与应用 输入、输出函数是一种常见的系统行为描述方法，把函数体作为系统过程，适于处 理顺序系统，然而面对并发系统时存在不足。如果两个并行的函数体在执行过程都操作 了一个系统变量，函数体的运行结果可能变得不确定，而不是原来每个函数体期望的确 定关系。产生混乱的原因是两个函数体通过操作一个系统变量而发生了联系，即它们之 间产生了交互。p i 演算描述并发程序时，摒弃了函数的观念，直接面对过程间的交互， 避免了用函数描述并发系统的弊端，增强了把握过程之间复杂关系的能力。 ( b ) 可描述过程结构动态变化 用交互式观念描述并发系统，能够直接描述过程之间结构动态变化，这是p i 演算最 突出的特点，它的图形描述可用流图表示。 p 、q 、r 是三个并发的过程( 图2 1 ) ，p 与r 通过连接a 进行通信，同时与q 通过连 接b 进行通信，初始状态时，r 与q 没有通信连接。 如果在p 的输出端口b 将连接a 输出，p 演变为p ，q 在输入端口b 接收连接a ，q 演变为q ，系统运行的结果为：a 的连接从p 与r 之间传递到q 与r 之间。 图2 1 过程之间结构变化的p i - 演算流图 f i g 2 1 t h ep i - c a l c u l u sf l o wc h a r to ft h ep r o c e s ss t r u c t u r ec h a n g e d 过程变化的表达式为：p - 品，t ，q - 6 0 ) q ；葫，i b ( y ) q - i r _ p l q i r 。其中t 表示 过程内部的一次通信。p i 演算把过程之间的连接作为传递对象，使旧连接消失，新连接 建立，从而改变了过程之间的结构。 ( c ) 可描述局部自治性 以往系统全局控制观念中，局部是被动地在全局支配之下。而并发系统是分布在不 同环境中执行的，它的局部具有自治性。因此以往全局状态的观念，已经无法描述分布 式系统的变化，需要引入局部状态描述。 大连理工大学硕士学位论文 p i 演算用绑定发生( b o u n do c c t l i t c r c c ) 描述局部变量，用自由发生o c c u r r e n c e ) 描述全局变量，便于描述局部自治与全局控制的关系。 ( d ) 基于过程代数公理的推演 p i 演算描述系统动态演进的过程，是基于过程代数公理的推演过程。观察等价、互 模拟及相关的一系列等价关系的定义，根据过程之间通信的物理背景产生，是公理形成 的基础。 从p i 演算的重要扩展公理可以看到，两个并发过程之间如果有通信的行为，系统 并发行为等价于它们子过程的分支选择行为以及内部交互。这种内部通信在外部观察不 到，也是函数观念处理并发系统时无法解释结果不确定性的原因。p i 演算深入到并发过 程的内部，以一系列公理对并发过程推演，对系统分析起着重要作用。 因此，p i 演算是并发、交互、并发系统的理论模型，它提供相关的概念框架和数学 工具，用于表达并发、交互系统和推论它们的行为，增强对并发系统的理解。 2 2 2p 卜演算的语法 我们用无限名字集合n 表示名字，它包括数据值、数据变量、数据常量、连接( 通 道) ，其上的变元使用小写字母，如：a 、b 、j 、y 等；进程也称为代理，标识集合a 表 示进程，使用大写字母表示，如：尸驮眉等【2 9 l 。 p i 一演算语法用b n f 给出： p ：o l x y p i x o , ) ，i f ，1 0 ) pi b - y p i p i q i p + q a 魄，以) 其中：o 是空运算符；一x y ，z ( y ) ，f 及b y 】是一元运算符；i 和+ 是二元运算符； n 是a 的元； 运算符的优先级也是以上的列出的顺序，即： 限制( r e s t r i c t i o n ) 1 前缀( p r e f i x ) 组颌国牺碱锄) 和跚瑚枷溉) 匹配( m a t c h ) j ( 1 ) o 表示空过程，不能实现任何动作。 ( 2 ) 前缀形式- y ，：“为 称为负前缀。名字；可以被看作一个进程的输出端口， 为，表示在端口；输出名字y ，然后执行p 进程。 前缀形式x o 妒：x ( ) ，) 称为正前缀。名字x 可以被看作一个进程的输入端口，x ( y ) 2 表 示在端口x 输入一个随意的名字，绑定到y ，然后执行p 进程。 哑前缀v p 表示执行哑动作f ，然后执行p 进程。 基于阼演算的无线自动售货机系统建模与应用 ( 3 ) 限制形式：表示除在端口z 和；的动作以外的动作被禁止。( 但是在p 组件 之间，沿着连接x 的通信不被禁止，因为他们已经成为了哑动作f ) 。 ( 4 ) 匹配形式b y p ：表示如果名字x ，y 相同，执行p 进程，否则执行0 进程。 ( 5 ) 组合形式p i q ：表示进程p 和q 并行执行。组件可以独立地执行，p 在任一个输 出端口；的一个输出可以与q 在x 端口的输入动作同步，产生一个组合p i q 的哑动作 ( f ) ( 6 ) 和进程形式p + q ：表示或者执行p ，或者执行q 。多于两个进程的和，可表示 为。 ( 7 ) 进程4 魄，以) ：表示进程标识符a ( 有f i 个元) 有一个独立的定义等式 么魄，y ) d e f p ，其中的名字咒，在p 种子有发生。定义等式可以递归，p 可以包含 任何进程标识符。 ( 8 ) 在x ( ) ，妒和o ，) p 形式出现的进程中，圆括号中y 的发生是绑定发生，发生范围是 尸。如果y 的发生不在绑定发生的范围，称为自由的。p 中的自由发生名字集合可表示 为f n ( p ) 。绑定发生名字的集合表示为b n ( p ) 。 ( 9 ) 名字替换是名字到名字的函数，p y x 表示在尸中用x 替换y 。 2 2 3p 卜演算的互模拟等价关系 p i 演算理论重心是行为等价理论，即如何判定两个并发执行、并与环境交互的系统 是否具有相等行为( e q u i v a l e n tb e h a v i o r ) 。如果两个系统行为相等，那么从任何环境取出 其中一个而放入另外一个，环境不会感知替换发生。研究行为等价理论的基本方法是 互模拟饵i s i m u l a t i o n ) 。p i 演算提供了两种行为等价理论：强互模拟等价关系和弱互模 拟等价关系。 ( 1 ) 互模拟 定义2 3 模拟( s i m u l a t i o n ) ：一个二元关系s 是模拟的，如果p s q 意味着： 1 ) 如果p - p t ，并且a 是一个自由动作， 那么对于一些q ，q q ，并且p 跑 2 ) 如果p 蚴一p - ，并且y 譬刀( p ，q ) ， 那么对于一些q ，q ! q ， 3 ) 如果p 虬p t ，并且y 譬以俨，q ) ， 那么对于一些q ，q ! 咄q ， 并且对所有的，p w y s q - w y ) 并且p 艘 大连理工大学硕士学位论文 其中，露仍q ) - 加( p ，q ) u 细僻q ) 也就是说，任何从p 的变迁必须被从q 的变迁模拟，这样，派生的p 和q - 保持着模拟。 定义2 - 4 互模拟( b i s i m u l a t i o n ) ：如果s 和他的逆都是模拟的，一个二元关系是一个 互模拟。记为二。 ( 2 ) 等价关系 p i 演算的行为分为两类：不可见的内部动作t 和可见的外部行为。内部动作描述系 统内部进程之间交互的能力；外部行为描述进程与环境交互的能力。应用p i 演算时， 感兴趣的总是系统的外部行为，强等价关系既考虑了系统的内部行为，又考虑了系统的 外部行为。弱等价只考虑系统的内部行为，p i 演算理论的主要目的就是判断两个具有不 同结构因而具有不同内部行为的系统是否等价。 定义2 5 等价( e q u i v a l e n c e ) ：如果1 6 和是互模拟的，p 和q 是等价的，其中，6 是替换，如 y l x ) 。记为p q 。 ( a ) 强等价关系 定义2 - 6 强模拟( s t r o n gs i m u l a t i o n ) ：设一进程集合上的二元关系s ，对所有p s q ， 如果有p 山p ，则存在留，并且g 山g 和p s q 成立，则s 称为强模拟。如果存在 强模拟s 并且p s q ，则称口强模拟p 。 定义2 7 强互模拟( s t r o n gb i s i m u l a t i o n ) ：如一变迁关系s 和它的逆都是强模拟，则 称s 为强互模拟。 定义2 8 强等价( s t r o n ge q u i v a l e n c e ) ：如果存在强互模拟关系s 和p s q ，则称g 和 p 是强等价或者称为强互相似，记为p 一鼋。 ( b ) 弱等价关系 定义2 - 9 经历关系( e x p e r i m e n tr e l a t i o n ) ：对任一se a c t ，定义关系号和关系辛如 下： c l e f a ：p 净q 表示存在0 个或多个约简序列p 呻_ q ，形式化定义为兮i + ， 即为一的传递自反闭包。 b ：设s 一吼口。，那么p 辛q 表示p 兮_ - - 1e 净二p n 兮q 。形式化定义为 sd e f a l口- 寺；辛一辛_ j 6 基于p i 演算的无线自动售货机系统建模与应用 定义2 1 0 弱模拟( w e a ks i m u l a t i o n ) ；设某进程集合上的二元关系s ，对所有p s q ， 如果有p ；p ，则存在留，并且g 辛g 和p s q 成立，i o s 称为弱模拟。如果存在弱模拟 s 并rv s q ，则称口弱模拟p 。 定义2 - 1 1 弱互模拟( w e a kb i s i m u l a t i o n ) ：如一二元关系s 和它的逆都是弱模拟，则 称s 为弱互模拟。 定义2 1 2 弱等价( w e a ke q u i v a l e n t ) ：如果存在弱互模拟关系s 和p s q ，则称鼋和p 是弱等价或者称为强互相似，记为p g 。 2 2 4p i - 演算的代数理论 口一变换( a l p h a - c o n v e r s i o n ) ap - q 表示p q ；( “- 是a 一可变换的，a - c o n v e r t i l b e ，入一演算中术语) 同余( c o n g r u e n c e ) c o 除输入前缀外，所有操作符保持= ； c 1 如果p z y - q z l y ，对所有z ，那么x ( y ) j - x ( y ) z 2 ； 和( s u m m a t i o n ) s op + 0 一p ： s 1p + p p ； s 2p + q t q + p ： s 3 ( p + q ) + 尺一p + ( q + r ) ； 限制( r e s t r i c t i o n ) r 1 o ) ( y ) p - ( y x x ) p ； r 2 如果x 诺加( p ) ，g ) 口，一口0 ) p ； r 3 o ) ( p + q ) 一o ) p + o ) q ； 匹配( m a t c h ) m 0i x y p 一0 i f x y m 1 i x - y 妒- p 平行( p a r a l l e l ) p o p 1 0 一p ； p 1p i q = q i p ； p 2 女果x 隹f n ( p ) ，( x ) ( p l q ) 一( x ) p l ( x ) q p 3 ( p i q ) i r p i ( q i r ) ； 大连理工大学硕士学位论文 扩展( e x p a n s i o n ) e 令p _ 啦丑，q - 岛锄，这里对于所有的f ，b n ( a d n n ( q ) 一妒，对于所有的 l j f ，锄( 声j ) f l f n ( p ) 一妒，那么 p i q 一啦假i q ) + p j ( p i q j ) * 。f 与，； j u l 。”掣卅 这里，关系q c d 胍p 乃( 吒c o m p e m e n t s l j ) 保持以下四种情况，业定义了r ，。 1 ) q 是毛，乃是z ) ；那么r ，是引g u v 2