（计算机软件与理论专业论文）非对称χlt≠gt演算符号互模拟验证.pdf

非对称) ( 演算符号互模拟验证 摘要 随着计算机技术和网络通信技术的高速发展，以并发性、分布性、实时性、异构 性和互操作性等为主要特征的并发分布式系统已经成为计算机技术的主流方向与此 同时，并发计算本身固有的复杂性，使得并发系统的研究和开发非常困难，系统的正 确性和可靠性难以得到保证 形式化方法是认识并发分布式系统，提高并发分布式系统正确性和可靠性的行之 有效的重要研究方法进程演算是一类重要的形式化方法著名的进程代数包括c c s 、 c s p 和7 r 一演算等 一演算是在c c s 基础上发展起来的一种移动进程演算以”一演 算为代表的进程代数，由于其概念简洁，可用的数学工具丰富和数学方法灵活，在并 发分布式系统的规范、分析、设计，验证和信息安全等方面得到了广泛的应用 x 一演算是”一演算的改进和发展从操作观点看，x 一演算是通过消除 一演算的非 对称性而得到的，是一种对称的移动进程演算这一改进导致观察性质的重要变化 有关x 一演算的研究丰富了类7 r 一演算的内容，这些研究有助我们增进对类x 一演算的认 识有关x 一演算的有意义的结果包括揭示弱观察等价关系的微妙差别，以及发现这 些关系的复杂规律但在现实的并发分布式系统中，绝大部分通信都是非对称的。并 且往往要求不等名测试，因此本文研究具有非对称通信和带不等名算子的x 演算，即 非对称x - 演算本文的主要工作包括以下三个方面， 1 参照傅育熙教授关于x 一演算的开互模拟定义。给出非对称x 一演算的强开互模 拟关系定义，以及其弱的版本定义 2 基于林惠民院士的符号化思想以及钟发荣老师关于非对称x 一演算的操作语义的 定义，给出非对称x 一演算的符号操作语义，并定义了符号强开互模拟、以及符 号弱的版本定义，并证明了符号开互模拟与其开互模拟关系是一致的 3 完成了带不等名测试算子的非对称x 一演算的符号强开互模拟的验证算法，证明了 算法的正确性 上述结果既具有重要的实际意义和理论意义；从实际上来看，我们的工作为开发非对 称x 一演算上进程互模拟等价关系的自动验证工具奠定了理论基础从理论上来看，我 们的工作说明了用符号化的方法来研究非对称x 一演算是可行的，为进一步研究符号化 方法在非对称x 一演算上的应用做了初步的探索 关键词： 进程代数，非对称x 一演算，符号互模拟，非对称性，形式化 t h ev e r i f i c a t i o no fs y m b o l i cb i s i m u l a t i o n si n a s y m m e t r i cx c a l c u l u s a b s t ra c t w i t ht h er a p i dd e v e l o p m e n to f c o m p u t e rt e c h n o l o g ya n dn e t w o r kc o m m u n i c a t i o n ，c o n c u r r e n ta n dd i s t r i b u t e ds y s t e m st h a tf e a t u r ec o n c u r r e n c ，, d i s t r i b u t i o n ，r e a lt i m e 。h e t e r o g e n e - i t ya n di n t e r o p c r a b i l i t yh a v eb e c o m et h em a i nd i r e c t i o no fc u r r e n tc o m p u t e rt e c h n o l o g y m e a n w h i l e ，t h ei n t r i n s i cc o m p l e x i t yo fc o n c u r r e n td i s t r i b u t e dc o m p u t a t i o nm a k e st h ei n v e s - t i g a t i o na n dd e v e l o p m e n to fc o n c u r r e n td i s t r i b u t e ds y s t e mv e r yd i f f i c u i t , a n dt h ec o r r e c t n e s s a n dd e p e n d a b i l i t yo fs u c hk i n do fs y s t e mi st o od i f f i c u l tt ob ea s s u r e d t h e r e f o r ea s s u r i n g t h ec o r r e c t n e s sa n dd e p e n d a b i l i t yo fs u c hk i n do fs y s t e mi sw h a ts h o u l db es o l v e du r g e n t l y m l i l ca p p l y i n gt h ef o r m a lm e t h o dt ot h es p e c i f i c a t i o na n dv e r i f i c a i o no fs y s t e m si sa ni m - p u r t a ma p p r o a c ht os o l v et h i sp r o b l e m t h ep r o c e s sa l g e b r ai sa ni m p o r t a n tk i n do ff o r m a l i z a t i o n t h ew e l l - k n o w np r o c e s sa l - g e b r a si n c l u d ec c s ，c s pa n d7 7 r - c a i c u l u s t h ep r o c e s sa l g e b r a ，s u c ha s7 r - c a i c u l u s 。i sw i d e l y a p p l i e dt os p e c i f i c a t i o nd e s c r i p t i o n ，a n a l y s i s ，d e s i g n ，v e r i f i c a t i o na n di n f o r m a t i o ns e c u r i t yo f c o n c u r r e n td i s t r i b u t e ds y s t e mb e c a u s eo fi 协c o n c i s ec o n c e p t s r i c ha v a i l a b l em a t h e m a t i c a l t o o l sa n df l e x i b l em a t h e m a t i c a lm e t h o d s t h ex - c a l c u l u si st h ed e v e l o p m e n to f7 ，r - c a i c u i n s f r o mt h eo p e r a t i o n a lv i e w p o i n t t h e x c a l c u l u si sas y m m e t r i cm o b i l ep r o c e s sc a l c u l u so b t a i n e df r o m r - c a l c u l u sb yr e m o v i n g a s y m m e t r yo ft h el a t t e r 1 1 l i sm o d i f i c a t i o nr e s u l t si ns i g n i f i c a n tc h a n g ei no b s e r v a t i o n a l p r o p e r t i e s m a n ya s p e c t so f t h ex - c a l c u l u sh a v eb e e ns t u d i e d t h e s ei n v e s t i g a t i o n sh e l pu st o i m p r o v eo u ru n d e r s t a n d i n go f7 r - l i k ec a l c u l u sf o rm o b i l ep r o c e s s e s i n t e r e s t i n gr e s u l t sa b o u t t h ex - c a l c u l u si n c l u d et h er e v e l a t i o no ft h es u b t l e t yo ft h ew e a ko b s e r v a t i o n a le q u i v a l e n c e r e l a t i o n sa n dt h ed i s c o v e r yo ft h ec o m p l e xl a w sf o rt h e s er e l a t i o n s b u ti nt h ec o n c u r r e n t d i s t r i b u t e ds y s t e m s ，m o s to ft h e mc o m m u n i c a t ew i t he a c ho t h e ra s y m m e t r i c a l l y , a n dt h e m i s m a t c hc o m b i n a t o ri so f t e nr e q u i r e d t h e r e f o r e ，w es t u d ya s y m m e t r i cx # - c a l c u l u s ，t h e x c a l c u l u sw i t ha s y m m e t r i cc o m m u n i c a t i o na n dm i s m a t c ho p e r a t o ri nt h i st h e s i s 1 1 圮m a i n c o n t r i b u t i o no ft h et h e s i si n c l u d e st h ef o l l o w i n gt h r e ea s p e c t s ： 1 i n s p i r e db yf uy u x i so p e nb i s i m u l a t i o n sd e f i n i t i o na b o u tx - c a l c u l u s ，w eg i v et h e s t r o n go p e nb i s i m u l a t i o n sd e f i n i t i o no fa s y m m e t r i cx - c a l c u l u s 。a n dt h ew e e kv e r s i o n 2 b a s e do nl i nh u i m i n g ss y m b o l i ci d e aa n dz h o n gf a r o n g o p e r a t i o n a ls e m a n t i co f a s y m m e t r i cx 产- c a l c u l u s 。w eg i v et h es y m b o l i co p e r a t i o n a ls e m a n t i ca n dd e f i n et h es y m - b o l i cs t r o n go p e nb i s i m u l a t i o n sa n dt h ew e e kv e r s i o na l s o a n dt h a nw ep r o o ft h a tt h e o p e nb i s i m u l a t i o n sc o i n c i d ew i t ht h es y m b o l i cv e r s i o n s 3 w ed e v e l o pv e r i f y i n ga l g o r i t h m sf o rs y m b o l i cs t r o n go p e nb i s i m u l a t i o n si na s y m m e t r i c x 尹- c a l c u l u sa n dg i v et h ep r o o fo fc o r r e c t n e s so ft h i sa l g o r i t h m s n ea b o v er e s u l t sa r co ft h e o r e t i c a ls i g n i f i c a n c ea sw e l l 鹪t h e o r e t i c a ls i g n i f i c a t i o n 。 f r o mp r a c t i c a lp o i n t o u rw o r kp r o v i d e sas o l i dt h e o r e t i c a lb a s i sf o rd e v e l o p m e n to fa u t o m a t e db i s i m i l a r i t yc h e c k e r s f r o mt h e o r e t i c a lv i e w , o u rw o r ks h o w st h ef e a s i b i l i t yo fa p - p l y i n gs y m b o l i cb i s i m u l a t i o nt oa s y m m e t r yx - c a l c u l u s o u rw o r kb r e a k st h ep a t hf o rt h e f u r t h e rr e s e a r c ho ns y m b o l i cb i s i m u l a t i o ni na s y m m e t r yx - c a l c u l u s k e y w o r d s ：p r o c e s sa l g e b r a ，a s y m m e t r yc h i - c a l c u l u s ，s y m b o l i cb i s i m u l a t i o n ，a s y m m e t r y i i i 符号说明 我们在这里列出了本文所用到的非对称x 一演算中的各种符号，其中页码表示该 符号的第一次出现所在页 o b f r 瓦，b ，苞， n 弦 i k - ) h ( 0 九( 一) s n n z o ) n z 瓦( 霉) y * ( y ) 屈 o n z p 西z p n z 尸 p jq ) j f ) 陋= y l p 【# y l e p + q o ) 户 y * p ( ”) 肛i 名 余名 名或余名 所有名的集合 所有余名的集合 特定实体的自由名集合 特定实体的约束名集合 特定实体的所有名集合 名的有限集合 自由输入动作 约束输入动作 自由输出动作 约束输出动作 自由更新动作 约束更新动作 t a u 动作 非活动进程 输入前缀算子 输出前缀算子 前缀算子 并发算予 局部化算子 等名算子 不等名算子 选择算子 约束( 输入输出) 辅助前缀 u p d a t e , 辅助前缀 约束l l p d a e 辅助前缀 8 8 8 8 8 8 8 8 汀8 8 8 8 8 8 8 7 7 7 7 7 7 7 7 7 0 o o r p a y 尸 q ，咒 p p d d i s ( c ) m a t ( c ) m i s ( ) m i s ( d ) 、。 i p ，妒 f y c y l 妒= 妒 妒兮妒 妒妒 暑，z ) 口 霉盯，口( 茁) p 口 如m ( 盯) r n g ( 盯) n ( 盯) a 内部通信辅助前缀 任意前缀算子 任意不舍更新算子的前缀算子 进程 进程集合 更新序列 区别 条件上的操作 条件上的操作 条件上的操作 区别上的操作 条件上的操作 条件 不等名序列【y c y x 】【s ，】的缩写，其中y = l ，) 妒逻辑蕴含妒 妒逻辑等价于妒 妒和币的连接 原子代换 代换 代换a 作用在名3 5 上 代换口作用在进程p 上 代换盯的定义域 代换盯的值域 代换一的所有名集合 标号转移 任意内部通信转移 弱转移 带内部通信可观察转移的缩写 x 一演算的符号迁移 黔演算的符号弱迁移 强开互模拟 弱迟开互模拟 弱早开互模拟 符号强开互模拟 v m 8 8 0 8幅圪屹!他也坫搭岱：2协：2 n n u n n n n 儿n u n 擂心n n 挣 1f当善丛磐叼q “之 毛 鲤 符号弱迟开互模拟 符号弱早开互模拟 语法相等 定义等式 2 0 2 l 8 1 0 学位论文独创性声明 本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得 的研究成果。论文中除了特别加以标注和致谢的地方外，不包含其他人或其他机 构已经发表或撰写过的研究成果。其他同志对本研究的启发和所做的贡献均已在 论文中作了明确的声明并表示了谢意。 研究生签名：善鸟终孑狡日期：伽1 ；、一f 学位论文使用授权声明 本人完全了解浙江师范大学有关保留、使用学位论文的规定，即：学校有权 保留送交论文的复印件和电子文档，允许论文被查阅和借阅，可以采用影印、缩 印或扫描等手段保存、汇编学位论文。同意浙江师范大学可以用不同方式在不同 媒体上发表、传播论文的全部或部分内容。保密的学位论文在解密后遵守此协议。 研究生签名：喜。茛施导师签名老中馅丞 日期：西畚，一。一 第一章引言 并行与并发计算模型是计算机科学研究的重要问题与顺序计算不同，我们对并 行并发计算实质的认识还处于初级阶段自m i l n e r 提出c c s 以来，计算机科学家提出 了许多并行与并发计算模型其中进程代数是一类比较成功的模型本文主要研究的 对象是进程代数中带不等名测试算子的x 演算( e px 一演算) ，研究的主要内容是x 演算符号开互模拟的验证算法 1 1 研究背景 计算机科学的目的是向人们解释计算系统的行为关于计算过程( 算法) 的研究远 比计算技术要早的多因此，计算机科学的许多方面在计算机发明之前就已经存在了 但是真正的可以存储程序的计算机的出现给我们提出了巨大的挑战如果我们能够在 计算机上正确地描述我们所想做的事情，那么这些工具就能为我们做大量的事情所 以，在表示数据和算法方面计算机科学取得了巨大的进步在这个过程中。技术成为 了计算机科学发展的催化剂 随着计算机技术和通信技术的高速发展，以并发性，分布性，实时性。异构性和互 操作性等为主要特征的并发分布式系统已成为当前计算机技术的主流方向。而高速发 展的i n t e m e t 更是一个全球规模的并发分布式系统此外，由于并发计算本身固有的复 杂性，使得并发系统的研究与开发变的十分困难，而系统的正确性和可靠性也难以得到 保证所以，如何保证复杂计算机软硬件系统的正确性和可靠性，是亟待解决的问题将 形式化方法( f o r m a lm e t h o d ) i j 应用于系统的描述( s p e c i f i c a t i o n ) 和验证( v e r i f i c a t i o n ) 。 是解决这一问题的重要途径形式化的并发理论主要研究并发系统的形式模型和形式 语义；该理论贯穿并行体系结构、并行处理并发编译、并发语言，并发编程等应用技 术中的理论问题形式化并发理论最集中地反映了计算机应用技术对计算机理论所提 出的同题的多样性形式化并发理论的两大分支是p e t r i 网理论和进程代数理论有关 并发系统的形式化研究可以追溯到2 0 世纪6 0 年代早期的p e t r i 网弘4 】7 0 年代，计 算机科学家开始致力于用代数的方法研究并发系统，并形成进程代数理论1 9 8 2 年， b e r g s t r a 和k l o p 在“进程代数的不动点语义。【5 】中首次提出进程代数这一术语，在 该文中，进程代数仅指在泛代数意义下满足一组特定公理的代数结构1 9 8 4 年后才特 指用代数方法研究并发系统的研究领域进程代数研究并发计算的代数模型。提供类 似子a 一演算的操作语义模型，进而研究并发进程的行为准则和语义解释 进程代数的研究热点集中于两个方面，一是关于各类演算本身的理论，二是探讨新 2 浙江师范大学硬士论文 颖的计算概念，如移动计算、分布计算、i n t e r n c t 计算、全球计算( g l o b a lc o m p u t i n g ) 网格计算等的语义模型移动性涉及二个领域，一是m o b i l ec o m p u t i n g ，它关心的是 利用移动的设备进行计算；二是m 0 b i l ec o m p u t a t i o n 。它研究的是代码在设备问的移 动基于通讯的并发计算模型，如c c s ，丌_ 演算和x - 演算等，比较适合描述m o b i l e c o m p u t a t i o n 一类的计算用代数方法刻画并发计算的模型包括通信顺序进程c s p 帆”， 通信系统演算c c s 【8 0 1 ，通信进程代数a c pi n - t 3 ，移动进程演算7 r - 演算【1 4 1 ，x - 演算 1 7 ，1 8 1 ，灰箱演算m o b i l ea m b i e n ti t 9 ，s p i 演算 2 0 l ，应用 f - 演算1 2 2 1 等进 程代数，由于其概念简洁、可用的数学工具丰富，在并发分布式系统的规范、分析 设计，验证和信息安全等方面得到了广泛的应用 1 2 进程代数发展历史 进程代数是一类刻画并发计算的代数模型并发计算模型的建立一直是计算机科 学领域的主要研究课题从六十年代的p e t r g 网【2 _ 4 】到七十年代末的c s p 【6 7 】和八 十年代初的c c s 【8 ，t o 直到九十年代的7 r 演算 1 4 l 及其改进版本x 演算 1 7 , 1 8 l 等， 并发计算模型的研究内容丰富多彩这里简要介绍主要的并发计算模型及其特点 1 2 1p e t r i 网模型 一些并发理论既给出并发模型又给出演算系统，如c c s 和c s p 等而p e t r i 网只 给出模型，而没有演算但是p e t r i 网是一种真并发模型它虽不能像程序那样执行， 不能像c c s 那样有漂亮的演算系统，但它可以刻画更多的并发现象，如并发、矛盾及 无死锁性等等。 p c t r i 网有两个基本要素，条件和事件每当一定的条件满足时，相应的事件便可 发生。然后原来的条件发生变化。一些条件从成立变为不成立，另一些条件又从不成 立变为成立，于是，又有一些新事件可以发生p e t r i 网用点火和转移规则描述系统从 一个状态到另一个状态的迁移一组事件之间如果没有因果关系，则可以并发点火 p e t r i 网描述的系统中不存在一个统一的时钟，这是网论的本质主要的p e t r i 网有两 种zc e 系统和p t 系统。c e 系统是条件事件系统的简称，具有良好的选择，如网 的格局( c a s e ) 间相通，且对每个事件都存在格局，使之能够在此状态下点火p t 系 统是位置变迁系统的简称，与c e 系统相比，p t 系统有许多特异现象，如 一个位置中可以有多个标码，一次变迁可以使多个标码沿弧流动； 同一变迁可以反复连续发生； 同一变迁可以“自我并发”地多重发生； 同一网结构可以既呈现矛盾又呈现并发 第一章引言 总的来说，利用p e t r i 网来验证系统的计算和语义特性较为困难不过，我们可以把 p e t r i 网描述并发的思想应用到刻画系统组件的交互之中 1 2 2c s p 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 ) 模型【6 】是h o a r e 创立的早于c c s 的计算 模型其跟c c s 的研究工作几乎是并行开展的c s p 模型是一种适用计算应用领域 的最简单的数学理论模型虽然这种模型能把计算机所涉及的各种计算形式及其性质 用一套严密的形式系统来模拟，但是它以进程中事件的顺序执行及进程间通讯为出发 点来研究并行计算的一般模式因此。其并行计算的能力也是有限的 1 2 3c c s 上世纪八十年代初。r o b i nm i l n e r 提出了通信系统演算c c s 【8 ，1 0 1 。c c s 通过通 信来刻画并发计算。所有的计算都由进程之间的通信来完成，而进程之间的并发理解 为通信动作的交错( i n t e r l e a v i n g ) 加上不确定性c o s 模型包括三个部分； 语法：定义进程的算子很少，仅包括前缀算子，不确定选择算子，并行复合算子， 约束算子，换标号算子，但具有较强的描述能力； 操作语义- 操作语义采用定义在进程上的标号转移语义3 5 1 ，即进程的行为由 标号转移系统表示； 语义等价关系：把具有同样行为的进程称为等同的进程 c c s 中的通讯采用。握手”方式来实现该模型的操作语义建立在标号迁移语义 ( 1 a b l e dt r a n s i t i o ns e m a n t i c s ) 上，所以这个模型可以很好地描述结构不变的并发系统 c c s 模型可以说是并发模型计算的一个重要里程碑，它对以后的并发计算模型的研究 产生了重大的影响 c c s 之所以能成功地应用于并发系统建模和程序验证。主要得益于基于互模拟概 念的行为等价语义理论的建立( d p a r k 【9 】) 和完善( r m i l n e r 1 0 】) 互模拟等价是进程 演算中最为重要的等价关系进程演算中大部分的研究就是围绕着互模拟等价这个概 念展开的根据是否忽略表示系统内部通信的r - 动作，互模拟等价又可以分为强互模 拟等价和弱互模拟等价，强互模拟等价关系要求两个系统互相模拟所有的动作，包括 内部通信动作；而弱互模拟等价关系则忽略f - 动作基于弱互模拟的观察同余关系是 实际应用中最重要的关系因为它所刻画的等价关系最接近人的直观 4 浙江师范大学硕：l - r e 文 1 2 4 1 1 - 演算 丌- 演算u 4 j 是对c c s 的扩展，它由m i l n e r 、p a r r o w 和w a l k e r 芒e e n g b e r g 和n i e l s e n 工作的基础上提出了的它在保持c c s 代数性质的同时扩展了其并发计算能力在 c c s 中，进程之间的通信只接收到数据而不能在以后的通信中用作通道名，而什演 算是一个封闭系统，它忽略了c c s 中通道和变量的差别而将它们统一为名( n a m e ) ， 故其基本的计算实体是名和进程，进程之间的通信是通过传递名来完成的由于可以 传递通道名，故此模型可以用来描述结构不断变化的动态系统 在7 r - 演算中有两类含义不同的约束名一类是形如( z ) p 的局部名，不能被实例 化；一类是形如o ( 可) 固的输入参数y ，y 只是一个占位子，可被实例化但作为约束 名，两者都可以进行a 一换名另外，因为约柬名的私有性。被限制的局部名不能作为 通道与外部通信。但能通过其它的通道向外界输出，进而将其辖域扩展到接收该局部 名的进程这一点也是与传值c c s 的主要差异。也是导致”- 演算表达能力丰富和语 义复杂的根源 1 - 2 5x - 演算 x - 演算t 1 7 1 8 , 2 4 , 2 5 1 是傅育熙教授提出的一种新颖并发计算模型，它建立在7 r 演 算的基础上，是对7 r 一演算研究工作的继续和发展，其基本思想与开演算相同，但与 一演算相比，它有如下特点， 1 取消了抽象名( a b s t r a c tn a m e ) ，将它和局部名合而为一 2 统一了输入和输出操作子，这样在该演算中名的输入操作可通过名的受限来完成。 即将一演算中的输入进程口( 2 ) p 表示( z ) o i x p ，因而x 一演算的通信具有对称的 性质，因x 一演算的语法结构更加简洁 3 x 演算中通过局部化操作来描述通信的代数语义，使互模拟这一重要概念的定义 更加简洁，证明更加方便，性质更加良好正因为它统一了卅演算中的进程的输 入和输出前缀，进程之间的独立程度得到加强静演算用信息交换的通信机制代 替了筇一演算中的进程之问传值的通信机制 舻演算可以看作p r o o f - a s - p r o c e s s 方法【1 6 】的反向即p r o c e s s a s - p r o o f 【1 8 】而 r e a c t i o ng r a p hl 2 3 j 则是x - 演算内在机制的一个形象的描述方法 在x 一演算中，傅育熙教授提出了3 1 个厶互模拟关系这3 1 个厶互模拟关系构 成了互模拟格( 缩减为4 个互模拟关系) ，它们的等式公里系统已经给出在非对称x - 演算中，共有6 3 个厶互模拟关系这些互模拟关系同样也构成了互模拟格( 缩减为 1 8 个互模拟关系) ，它们的等式公理系统也已经给出文献 2 8 1 研究了带( 不带) 不等 名测试算子的x - 演算上的符号弱迟开互模拟，并证明它们和各自演算中的开互模拟是 第一章引育 一致的文献【2 9 】系统地研究了带不等名测试算子的演算上的弱早开互模拟和弱 迟开互模拟的符号互模拟的符号互模拟刻画文，【3 0 】比较系统的研究了非对称x 演 算的代数语义，定义了菲对称x - 演算语义和语法，系统的研究了非对称x - 进程的互 模拟相等性以及g r o u n d 互模拟和互模拟格底部的其他五个l 一互模拟的代数语义 上述的代数理论( 除p e t r i 网模型) 都统称为进程代数，其共同特征为， 1 、都使用通信，而不是共享存储空间，作为进程之间相互作用的基本方式，集中 表现了并发和分布式系统的特点； 2 、在语法上，使用一组算子作为进程的组件；算子的语义采用结构化操作语义 m 3 5 j 方法定义；进程可看作标号转移系统； 3 ，把并发性归结为非确定性，个并发执行的进程，其行为被看作是各单个进 程行为的所有可能的交错合成。即所谓的交错式语义 1 3 本文研究内容和成果 具有同样的输入、输出前缀形式和通信的对称性是廿演算的一大特点理论上具 有同样的输入、输出前缀形式和通信的对称性是x - 演算的个完善的性质但在实际 的程序设计中，往往需要非对称的通信方式，也就是说，必须严格区分输入和输出动 作；同时。相同的前缀形式和通信的对称性可导致额外的不确定性，这是不希望看到 的傅教授对非对称性x 一演算做了进一步的研究2 7 这些研究表明，非对称x - 演算的代数理论比对称x 一演算要丰富得多本论文主要研究的内容是非对称带不等 名算子的x 一演算的符号互模拟，即x 演算的符号互模拟验证算法本文的主要成果 有t i 非对称矿一演算的开互模拟 定义了非对称矿一演算的强开互模拟关系，弱迟，早开互模拟关系 2 非对称x 。演算的符号操作语义和符号开互模拟 根据非对称x - 演算的操作语义，定义了非对称矿演算的符号操作语义，并强 调通信的非对称性，即区分通信的输入和输出动作同时也定义了符号强开互模 拟关系，符号弱迟，早开互模拟关系并证明了符号开互模拟与其开互模拟关系是 一致的 3 给出了非对称演算的符号强开互模拟的验证算法 给出了算法的伪m e 描述，并给出了算法的正确性证明 1 4 本文结构 本文共分五章。除本章外，其余各章组织如下t 6 浙江师范大学硬士论文 第二章给出非对称x 一演算的语法和语义以及其开互模拟的定义； 第三章着重研究了非对称x 演算符号化，定义了非对称矿- 演算的符号操作语 义；随后定义了非对称x 一演算的符号强开互模拟关系，符号弱迟，早开互模拟关系， 并证明与其对应的互模拟关系一致的t 第四章研究了非对称矿一演算的符号强开互模拟验i 正算法，并给出了算法的正确 性证明 、 第五章总结了本文的主要贡献，并阐述了未来研究方向 2 1 引亩 第二章非对称x 演算 x 一演算是傅育熙教授提出的一种新型的并发计算模型，它建立在7 r - 演算的基础 上，是对7 r 一演算的研究工作的继承和发展从操作观点看，x 一演算是通过消除7 r 演 算的非对称性而得到的这一改进导致观察性质的重要变化已有一些文章从多个角 度研究了x 一演算瞄，2 7 , 2 9 , 鲫，这些有助于我们增进对一演算的认识假设z s ， 在x 演算中，有如下归约， p ) ( o z p i 瓦暑，q l r ) ( ) ( o z p l 瓦q l r ) 扣) 口z pi 西q ( z ) 蔬z pio 耖q p z iq y z in u l z p t z iq z u ir z y p t u l = l q p 可2 ) i q ( 2 1 ) ( 2 2 ) ( 2 3 ) ( 2 4 ) 在进程( 2 ) ( n o p l 动qi 冗) 中，名z 是受约束算子( z ) 约束的约束名；而d 岔p 和动q 是以前缀形式出现的进程，这里的z 和y 是自由名o z p 和 a y q 的交互致使约束算 子( z ) 作用到的整个复合进程中的霉被代换成y 在式( 2 3 ) 和( 2 4 ) 中，由于q 不受 ( $ ) 约束，交互的结果对q 没有影响这是因为在x 一演算中，其通讯方式是对称的，也 就是它并不区分输入和输出动作但在实际的程序设计中，往往需要非对称的通信方 式，也就是。必须严格区分输入和输出动作因此。在我们的菲对称x - 演算中，它不 允许式( 2 2 ) 和式( 2 4 ) 发生而本文主要讨论带不等号的非对称x 一演算的有关内容， l l p , 非对称x 一演算 本章的结构安排如下：在第2 2 节中介绍非对称x - 演算的语法；在第2 3 节中介 绍非对称一演算的操作语义，其由标号转移系统给出；在第2 4 节中引入区别概念， 给出非对称矿一演算的强开互模拟关系，弱迟开互模拟关系和弱早开互模拟关系；在 最后一节中对本章内容进行了小结 2 2 非对称x - 演算的语法 非对称x - 进程由下面的抽象语法定义t p ：= oio 口pl 尸ip i ( x ) pl 囟= 鲥pjk 圳pip + 尸 上述语法中的这些算子表示的含义和7 r 一演算的算子含义大致相同，其中， 0 表示非活动进程，该进程不做任何动作i 7 8 浙江师范大学硬士论文 q z p 是有动作前缀的进程如果口z = 孤。则该进程在通道口上输出名z 。然后 执行子进程p ；如果a z = ，则该进程可在通道。上接受名，然后执行后续 进程p y x ； p ip 是并行复合进程，复合进程中的两个子进程既可以彼此独立地执行，也可以 通过一个公共通道相互通信； ( x ) p 表示进程p 中的名z 受约束算子( ) 的约束，在进程( z ) p 中名$ 作为进程 p 的内部名使用，而无需担心来自其他进程的干扰； 【x = y p 表示当z 和y 同名时该进程为p ，否则为0 陋= 们为等名测试算子； f 茹引尸表示当名茁和y 互异时该进程为p 。否则为0 p 圳称为不等名测试算 子也将等名和不等名算子统称为条件算子； p - i - q 为不确定选择进程，该进程表示或者选择子进程p ，或者选择子进程q 一旦某个t - 进程被选中。则另个子进程被丢弃 非对称x 一演算有两类对象名和进程非对称矿一演算可看成通过统一霄一演算 的这二类约束名而得到的带不等名算子的演算，其方法是统一输入和输出动作的前缀 形式非对称x 一演算中，动作前缀具有口茹p 形式。这里口是指名a 或余名苞令 表示名的集合，集合中的元素用小写英文字母表示，刀表示余名的集合 _ iz ， 希腊字母口表示集合u 刀中的元索对于a u = 耵，如果a = 西，那么西定义为 a ，如果理= d ，那么西定义为瓦用p ，q 。r 表示非对称x - 演算的进程，而p 表示非对称x 一进程的集合 2 3 非对称x 一演算的语义 非对称x 一演算的操作语义【则由下表2 1 1 给出的标号转移系统脚，3 5 】定义这 里省略了所有对称规则系统中的这些规则规定了进程在交互过程中其拓扑结构的变 化方式 设a 表示转移标号集 a x ，酏，a ( z ) ，西( 霉) ，肛，( y ) 肛l 口，耖) u r ) 中的元索， 7 表示转移标号集 o z ，西霸n ( 茁) ，_ ( z ) ia ，z u r ) 中的元索在转移标号掣肛和 ( y ) 肛中，名$ 和y 互异出现在形如口( z ) 或( z ) 乃的动作a 中的名茁是约束的；否 则它是自由的我们用6 n ( a ) 。，n ( a ) 和n ( a ) 分别表示a 中出现的约束名集、自由名 集和名集集合概( 7 ) ，f n c t ) 和n ( 7 ) 的定义类似类似地，可以很容易地定义进程 p 中的约束名集h ( p ) 、自由名集f n c e ) 和名集n ( p ) 事实上，约束名只是个占 位符号本文采用a 一变换约定，即进程中的约束名可以用新名来代换如果进程p 和 q 是n 一变换的，记为尸三q 蔓三塞斐壁窭羔兰二煎蔓! 顺序 复合 通信 表2 一l 非对称- 演算的操作语义 n t j p 竺ps q r t p i pq q 二7 i p ! 生p i 了而亚i 而群唧 p 唑p u 口t i k q ) 7 面亚再币丽咖。 p 蛆p ，q 马q ，p 塑p ，q 鸳q ， 1 可石_ 二三了曩历i 汀石芦m ”o1 可否= 互1 习i 万i 巧叫”1 p 二p 7 ，q 兰垡垡爹p 二p ，q 三。 雨卫历瓦西雨丽g m 化i 百= 7 雨_ 叼m m 3 1 p 箍i q 篙胬i 祭q弛，堕骘p ， y 肛7 掣肛 一 ， 条件 选择 p ! 竺p ，$ 茹 口，石) p ! ! s p ， 一 1 面疆甄一岘百万= p ! 生p ， 百万巫历o c s p 吆p ， 一 丽f 二而山响 ；辜等胁矾 啬冬争胁一黼i ；万= 骄厂胁矾 再而乏e 书一胁一把 p _ p l 了干万! “m 标号转移系统中使用了七种动作标号，它们分别为 ( 1 ) 符号口z 。表示自由输入动作，即通过通道。输入一个自由名。； ( 2 ) 符号o ( 毒) ，表示约束输入动作，即通过通道口输入一个约束名$ ； ( 3 ) 符号勖，表示自由输出动作，即通过通道a 输出一个自由名o ； 1 0 浙江师范大学硬士论文 ( 4 ) 符号西( 霉) ，表示约束输出动作，即通过通道d 输出个约束名z ； ( 5 ) 符号屈，表示自由u p d a t e 动作，即用自由名y 代换自由名茁； ( 6 ) 符号屈，表示约束t l p d a ? 也动作。即用约束名y 代换自由名o ， ( 7 ) 符号r ，表示t a u 动作。即内部通信动作 下面简单介绍标号转移系统中每条规则的含义顺序规则说明t 进程d z p 必须 在完成动作a 留之后，才能做后续进程p 的所有可能的动作三条复合规则描述了这 样一种情况t 复合进程中的每个进程都可以相互独立地演进由于自由u p d a t e 和约束 u p d a t e 动作对邻近进程产生副作用，故对这两个动作进行单独处理在规则c m m o 和 g m m l 所定义的通信中。c m m o 描述一个进程接收其它进程所发送的自由名，而规 则c r a m l 规定个进程接收其它进程发送的约束名；规则c r a m 2 和c m m a 分别引入 自由u p d a t e 和约束u p d a t e 动作，在结构化语义定义中，这两条规则改进了语言通信的 定义为了简化非对称矿一演算的代数语义而增加的规则c r n m 3 ，可以看作为规则 c r a m 2 的补充自由u p d a t e 动作知是在文 1 5 ，1 7 中为定义标号转移语义中的通信 首次引入的。而约束u p d a t e 动作( 掣) 肛则是傅教授在研究非对称x 一演算【冽时引入 的自由u p d a t e 动作和约束u p d a t e 动作都是不完全通信动作【”，l j 7 ，2 6 1 ，是观察者所看 到的部分通信，可以将其理解为“正在发生但还没有完成的通信”或者“从内部看到的 通信”一旦自由u p d a t e 和约束u p d a t e 动作遇到约束算子，通信就完成了由此也可以 看出，约束算子不仅具有约束，限制的作用，而且也起到了界定通信范围的作用规