（计算机应用技术专业论文）面向模型的组合理论研究.pdf

2 0 11d o c t o rt h e s i s ir llr l li i i iil rl l liij y 19 0 5 2 8 3 。 s c h o o lc o d e ：10 2 6 9 s t u d e n tn u m b e r ：5 2 0 815 0 0 0 0 7 i i l a tc 丑n an r m a lu n r t v m o d e l0 r i e n t e dc o m p o s i t i o n d e p a r t m e n t ： m a j o r ： s u b j e c t ： 而f o r ： a u t h o r ： t h e o r y s o f t w a r ee n g i n e e r i n gi n s t i t u t e c o m p u t e ra p p l i c a t i o nt e c h n o l o g y f o r m a lm e t h o d s p r o f h ej i f e n g “q i n 2 0 11 4 华东师范大学学位论文原创性声明 郑重声明：本队呈交的学位论文面向模型的组合理论研究，是在华东师范 大学攻读硕士z f , j 2 - 生( 请勾选) 学位期间，在导师的指导下进行的研究工作及取得 的研究成果；除文中已经注明引用的内容外，本论文不包含其他个人已经发表或 撰写过的研究成果。对本文的研究做出重要贡献的个人和集体，均己在文中作了 明确说明并表示谢意。 x 厶， 作者签名：壹丝日期：y f j 年j _ 月玎日 华东师范大学学位论文著作权使用声明 面向模型的组合理论研究系本人在华东师范大学攻读学位期间在导师指 导下完成的硕士鹄缶( 请勾选) 学位论文，本论文的研究成果归华东师范大学所 有。本人同意华东师范大学根据相关规定保留和使用此学位论文，并向主管部门 和相关机构如国家图书馆、中信所和“知网”送交学位论文的印刷版和电子版； 允许学位论文进入华东师范大学图书馆及数据库被查阅、借阅；同意学校将学位 论文加入全国博士、硕士学位论文共建单位数据库进行检索，将学位论文的标题 和摘要汇编出版，采用影印、缩印或者其它方式合理复制学位论文。 本学位论文属于( 请勾选) ( ) 1 经华东师范大学相关部门审查核定的“内部”或“涉密”学位论文木， 于年月日解密，解密后适用上述授权。 劬2 不保密，适用上述授权。 导师签名本人签名：魄 口f f 年r 月心日 木“涉密”学位论文应是已经华东师范大学学位评定委员会办公室或保密委员会 审定过的学位论文( 需附获批的华东师范大学研究生申请学位论文“涉密”审 批表方为有效) ，未经上述部门审定的学位论文均为公开学位论文。此声明栏不 填写的，默认为公开学位论文，均适用上述授权。 姓名职称单位备注 缪为丕和 劾彳蚕乡诲尺参 主席 怨遭珲 私者爱乡妇叠妙尺季 如黔私才云 舒巧、】印如六善 玉1 袖 瓠梧 辞身，、) 印茹乒季 霹式肚彬孝i 援 乍彝、i 彳宓凡冢 摘要 随着计算机科学与软件工程的飞速发展，人们越来越强烈的意识到形式化模 型对软件系统的分析与设计的重要作用。在当今软件系统的设计与开发中，人们 普遍运用多种建模方法和工具对软件系统本身及其应用场景建立模型，并在这些 模型的基础上对系统进行分析和改进。对于一个复杂的软件系统而言，一个使设 计者和开发者都能正确认识和分析该系统的模型在软件开发周期中显得尤其重 要。 一个涵盖系统所有要素的模型往往不易获得。系统设计者通常是先将系统按 照一定的特征划分成很多部分，再分别对这些部分采用适当的建模方法和工具建 立相应的模型。该研究思路很好的使用了分而治之的策略，有效的降低了处理系 统具体特征的复杂度，使针对某个特征的分析和推理变得方便。然而，由于针对 各个系统特征的建模方法都是独立发展起来的，往往依赖于不同的数学基础，这 使得我们在面对使用不同建模方式建立的模型时，很难将他们的信息进行共享和 协调，从而得到我们所期望的系统的整体视图。 为了解决这个问题，我们需要一个精确而系统的理论框架来描述模型之间的 关系，支持模型之间信息的共享和交互，实现模型的融合与协调。 本文旨在提出一个针对软件系统的模型组合理论，使得模型之间的各种组合 模式都能够在该理论下得到解释，进而可以在该理论的支持下讨论模型之间的关 系以及各种模型组合方式所具有的性质和特点，为模型组合实践中组合模型表现 出来的良好性质给出理论依据。该模型组合理论框架不仅能够描述某个模型所涉 及的各种系统属性及属性间的关系，而且能够分析不同模型间的联系，帮助我们 进一步认识和理解现有模型的特点以及他们之间的关联性，研究模型的某些特殊 性质在模型组合过程中的演化情况。有了该理论框架的支持，设计者可以根据设 计需要对模型进行适当的调整，将它们组合成满足特定需求的组合模型。另外， 对该理论框架的研究可以指导软件设计者和开发者，统一两者对软件系统的认识， 消减模型中的不确定性，显著提高软件系统的设计、开发与验证效率。 本文的主要内容包括： 提出一个针对软件系统的模型表示框架，每个模型针对软件系统的特定属 性，根据系统在这些属性上表现出来的可见观察对系统行为进行刻画。模型 中既包含了每个研究对象的组成结构信息，又包含了对象之间的运算和关系 信息，具有解释与对象相关的全局性质与局部性质的能力。我们使用该模型 表示框架表示了很多建模模式如状态转换模型和事件反应模型等。 考察了包括程序组合、服务组合等软件工程领域中关于组合问题的解决方 案，吸取了软件工程领域中对这些组合问题的处理经验，总结出组合问题的 普遍特征，进而引入模型层次上的组合概念，研究以模型为基本对象的模型 扩展、模型融合和模型补全等模型组合方式，以及它们所具有的普遍性质。 关键词：模型，组合理论，形式化方法，程序统一理论 a b s t r a c t w i t ht h er a p i dd e v e l o p m e n to fc o m p u t e rs c i e n c ea n ds o f t w a r ee n g i n e e r i n g ，t h e r ei sa g r o w i n ga w a r e n e s so ft h ei m p o r t a n ti n f l u e n c eo ns o f t w a r ea n a l y s i sa n dd e s i g n i n gm a d eb y f o r m a lm o d e l s m a n ym o d e l i n g m e t h o d o l o g i e sa n dt o o l sa r ee m p l o y e dt om o d e lt h er e a l w o r l ds c e n a r i o sw h e nd e s i g n i n ga n dd e v e l o p i n gm o d e r ns o f t w a r es y s t e m s t h em o d e l s a r ea l s ou s e dt oa n a l y z ea n di m p r o v et h es o f t w a r es y s t e m s i ti se s s e n t i a lf o rt h ed e s i g n e r s a n dd e v e l o p e r st oh a v eap r o p e rm o d e lf o ra c o m p l e xs o f t w a r es y s t e m s u c ham o d e lc a n h e l pt h e mg a i nac o r r e c tv i e wo ft h es y s t e mi ni t sd e v e l o p m e n tc y c l e s i n c ei t i sd i f f i c u l tt oa b s t r a c tam o d e lc o v e r i n ga l lr e q u i r e ds y s t e ma t t r i b u t e s ，t h e d e s i g n e r su s u a l l yd i v i d et h e 备y s t e ma c c o r d i n gt oc e r t a i nf e a t u r e sa n de s t a b l i s hm o d e l s f o re v e r yc o m p o n e n tw i t ha p p r o p r i a t ea p p r o a c h e sa n dt o o l s t h i su s eo fd i v i d ea n d c o n c u rs t r a t e g ys i g n i f i c a n t l yr e d u c e st h ec o m p l e x i t yo fd e a l i n gw i t hc o n c r e t es y s t e ma t t r i b u t e sa n df a c i l i t a t e st h ea n a l y s i sa n d r e a s o n i n go fs p e c i f i cs y s t e mp r o p e r t i e s m o d e l i n g m e t h o d o l o g i e sc o n c e n t r a t i n go nd i s t i n c ts y s t e ma t t r i b u t e s ，h o w e v e r , a r eo f t e nd e v e l o p e d i n d e p e n d e n t l ya n dr e l yo nd i s s i m i l a rm a t h e m a t i c a lf o u n d a t i o n s w ef i n di th a r dt os h a r e t h ei n f o r m a t i o nf r o mv a r i o u sm o d e l sa n dl e tt h e mc o o p e r a t ew i t he a c ho t h e rt oo b t a i nt h e e x p e c t e dg l o b a lv i e wo ft h es y s t e m t os o l v et h i sp r o b l e m ，ap r e c i s ea n d s y s t e m a t i ct h e o r e t i c a lf r a m e w o r ki si n d i s p e n s a b l et od e s c r i b et h er e l a t i o n s h i pa m o n gt h e s em o d e l i s m s t h ef r a m e w o r ka l s on e e d st o s u p p o r tc o n s t r u c t i n gp a r t i c u l a rm o d e li n t e g r a t i o na n dc o o r d i n a t i o np a t t e r n sw i t hi n f o r m a - t i o ns h a r i n ga n di n t e r a c t i o na m o n gm o d e l s t h em a i nm o t i v a t i o no ft h i sp a p e ri st op r o p o s ea t h e o r yf o ri n t e g r a t i n go rc o o r d i - n a t i n gd i f f e r e n tm o d e l so fs o f t w a r es y s t e m s t h et h e o r yn e e d st oi n t e r p r e tt h er e a s o n a b l e m o d e lc o m p o s i t i o np a t t e r n s ；a n ds u p p o r tt h es t u d yo ft h er e l a t i o n s h i pa m o n gd i f f e r e n t m o d e l sa sw e l la si n t e r e s t i n gp r o p e r t i e so fc o m p o s e dm o d e l si nm a n yp r a c t i c a ls c e n a r i o s t h et h e o r yh a sac a p a b i l i t yt od e s c r i b et h es y s t e ma t t r i b u t e sa sw e l la st h e i rc o n n e c t i o n s a n di n v e s t i g a t et h er e l a t i o n sb e t w e e nd i s t i n c tb e h a v i o r a lr e p r e s e n t a t i o n s w i t ht h i st h e o r y , w ec a nu n d e r s t a n dt h ef e a t u r e so fe x i s t i n gm o d e l sa sw e l la st h e i rc o n n e c t i o n sd e e p l ya n d s t u d yt h ee v o l u t i o no fs p e c i f i cp r o p e r t i e sd u r i n gt h em o d e lc o m p o s i t i o np r o c e s s t h i s t h e o r yc a na l s os e r v ea sag u i d et oa d j u s tt h ee x i s t i n gm o d e l sa n dc o m b i n et h e mt oo b t a i n c o m p o s e dm o d e l ss a t i s f y i n gp a r t i c u l a rr e q u i r e m e n t s f u r t h e r m o r e ，t h et h e o r yc a nc o n t r i b u t et oa c h i e v i n gu n i t yi np e r s p e c t i v e so fs o f t w a r ed e s i g n e r sa n ds o f t w a r ed e v e l o p e r s ， a n dr e d u c i n gt h en o n d e t e r m i n i s mo ft h em o d e l i n ga n dd e v e l o p m e n t h e n c es i g n i f i c a n t l y i n c r e a s i n gt h ee f f i c i e n c yo fs o f t w a r ed e s i g n i n g ，d e v e l o p m e n ta n dv e r i f i c a t i o n 1 n a n ds e r v i c ec o m p o s i t i o ni ns o f t w a r ee n g i n e e r i n gf i e l da n dl e a r nt h e i re x p e r i e n c e w e c a p t u r et h eg e n e r a lf e a t u r e so fc o m p o s i t i o ni s s u e sa n di n t r o d u c et h ec o n c e p to f m o d e lc o m p o s i t i o n t h ec o m p o s i t i o nt h e o r ya p p l y i n go nm o d e l si n c l u d e sm o d e l e x t e n s i o n ，m o d e li n t e g r a t i o na n dm o d e lc o m p l e t i n g i ts h o w sh o wt oc o m b i n et h e i n f o r m a t i o nb e t w e e nd i f f e r e n tm o d e l sa n de s t a b l i s hc o m p o s e dm o d e l sw i t hs p e c i f i c p r o p e r t i e s k e yw o r d s ：m o d e l ，c o m p o s i t i o nt h e o r y , f o r m a lm e t h o d s ，u n i f y i n gt h e o r i e so fp r o g r a m m i n g 。 i v 第二章模型表示框架 1 3 2 1 模型的概念1 4 2 2 模型的形式表示1 9 2 3 模型表示框架的应用2 6 2 3 1 状态转换模型2 7 2 3 2 事件反应模型3 0 2 3 3 结构模型3 5 2 4 本章小结3 6 第三章模型组合理论 3 9 3 1 模型扩展。4 1 3 1 1 横向扩展4 1 3 1 2 纵向扩展4 3 3 2 模型补全4 8 3 2 1 模型信息转换4 9 3 2 2 模型晋升5 1 3 3 模型融合5 7 3 3 1 正交融合。5 8 3 3 2 非正交融合6 0 3 4 本章小结6 1 v 第四章 4 1 4 2 4 - 3 第五章 5 1 5 2 5 3 5 4 5 5 理论应用：o r c 程序语言的语义模型 o r c 语言的指称语义模型 4 1 1 o r c 模型属性集 4 1 2 o r c 模型论域 4 1 3 o r c 模型特征映射定义 o r c 程序理论 本章小结 理论应用：基于总线的服务系统模型 服务计算行为模型 总线状态转换模型 总线系统事件反应模型 总线系统融合模型 本章小结 第六章总结与展望 参考文献 致谢 玫读博士学位期间发表论文和参与科研情况 3 4 5 9 3 7 2 5 8 1 3 6 8 9 b 1 5 矗6 8 7 7 8 & 8 9 9 9 9 9 o 1 1； 第一章绪论 弗一早珀v 匕 人们在研究一个新的复杂问题时普遍采用的科学方法是将该问题分解成多个 子问题，使得每一个子问题都能够使用己知的方法进行研究。这在数学、物理学、 化学等基础学科中相当普遍和自然，因此在这些学科中存在一个系统的方法论， 即首先将研究对象按照一定的方式分解成一个个简单的数学结构，这些数学结构 所表现出来的性质与研究对象实际的物理性质一一对应。进而，通过构造相应的 组合结构，使得这些简单结构之间的组合能够体现出研究对象整体的性质。换句 话说，研究对象可以由一些满足特定规则的数学结构组合而成。例如，任何物质 都是由原子按照一定的规律组合而成，原子的不同组合形式决定了不同物质所表 现出的不同的性质，而不同物质化学性质的差异则源于原子内部组成的差异，即 组成原子的更加微小的结构，如质子、中子和电子的数量、位置等因素的差异。 现代物理学的长足发展得益于组成物质的基本粒子的发现及在此基础上的理 论框架的建立。物质的运动规律和性质可以解释为组成物质的基本粒子的相互作 用状态。基本粒子的理论模型使得对同一物理系统的不同方面或不同层次的研究 能够独立进行，并统一于一个理论框架内。现代化学也有类似的统一理论框架， 如对组成物质的基本化学元素的研究，使化学过程可以被解释为元素之间的相互 作用，生成的新的化学物质也是由基本组成元素构成的。现代生物学也主要依赖 于对d n a 和遗传因子的研究，生物性状的产生和变异可以归结为d n a 的组成结构 和演化过程。由此可见，一个统一的基础理论框架对于现代科学的发展是至关重 要的，它奠定了这些学科的基石，使得该领域范围内的所有问题，不管多么复杂， 都可以归结到这个统一的理论框架下进行研究。 计算机科学技术从上世纪中叶开始起步，经过了半个世纪的发展，其发展速 度和普及程度与其他基础学科如数学、物理学和化学相比较是非常惊人的。普通 人在稍加训练后就能够使用计算机编写简单的程序，管理信息资源等，这些进步 在很大程度上归功于软件工程技术的迅猛发展。随着应用领域的不断扩大，各种 针对不同应用场景的程序语言如雨后春笋般进入工业应用领域。令人担忧的是， 在快速应用的同时，这些语言的使用者对语言本身语义的把握并不是非常明确的， 甚至有些语言在实现过程中就会出现功能与设计要求不符的危险情况。究其根本， 件系统的整体行为，难以检验系统行为是否满足给定的需求规范，软件的正确性 得不到保证。因此，我们需要一个系统的模型组合理论来指导不同模型间的信息 共享和综合，使得最终系统的性质能够在一个统一的理论框架下进行讨论。 我们希望本文能够在这样一个背景下，研究各种描述软件系统的模型及其之 间的关系，为建立一个系统的基于模型组合的理论框架做出一些贡献。 2 第一章绪论华东师范大学博士学位论文 1 1 基于模型的研究现状 关于模型的研究由来已久，很多成熟的形式化方法将重点集中在对软件系统 的建模和分析上，如系统性质的表达方式，系统行为的模拟，如何验证系统行为 符合规范需求等。针对具有不同特征的系统，研究者设计了多种不同的方法对系 统的行为和性质进行研究。 模型论( m o d e lt h e o r y ) 【2 4 ，6 9 ，s 7 是一种研究模型与形式语言的学科，起 源于逻辑学，现在它的主要的几个子学科包括经典模型论，面向群和域的模型 论，几何模型论和可计算模型论等。它研究具有特殊性质的数学结构( s t r u c t u r e ) ， 如群、域、图等，如果这些结构能够解释特定的形式语言中的语素，则称这些 结构为该语言的模型。特别的，如果该结构能够解释某个理论中所有的叙述 ( s e n t e n c e ) ，该结构被称为该理论的模型。模型论对模型的定义指出模型是理论 的解释工具，由数学结构和泛代数两部分组成，采用逻辑方法对语义对象进行研 究，形成了完备的逻辑系统。使用模型论中的结论，我们可以研究模型与形式语 言之间的关系，验证某个具体模型是否满足特定的理论。与模型论类似的应用 于计算机科学的理论还有类型论( t y p et h e o r y ) 【2 5 ，9 0 ，证明论( p r o o ft h e o r y ) 【9 5 ，9 2 1 等，它们是程序语言中的数据结构和类型系统的理论基础之一。本文中讨 论的模型概念源于模型论中的定义，并针对软件系统的特点提出了更加适合解释 软件系统性质的模型结构。 统一建模语言u m l 是对象管理组织( o m g ) 提出的一种描述软件系统的可视 化建模标准，主要用于面向对象的软件系统设计 1 7 ，1 6 。u m l 提供了很多针对软 件系统的建模手段，这些手段一般采用直观的图表方式给出，能够使用不同的模 型分别表示软件系统的组织结构，动态行为和交互情况。将这些模型综合起来， 设计者就可以得到系统的整体蓝图。u m l 中比较常用的模型有描述系统结构的类 图、对象图、组件图等；描述对象动态行为的状态图、活动图、用例图等；描述 对象间交互行为的顺序图、通信图等。u m l 中提出的模型分别侧重于系统的不同 方面，采用直观的方式表现系统在该方面的行为特征，帮助软件设计者和开发者 从不同的角度准确理解系统各个方面的设计意图。即便都属于描述对象间交互行 为的模型，顺序图和通信图也有各自不同的侧重点：顺序图强调的是交互消息的 时序，而通信图强调的是对象的组织结构以及在交互中的角色。这些模型可以彼 此独立存在，也可以根据他们之间的联系进行综合。描述同一软件系统的模型中 的类和对象具有相同的名称和成员，对象的内部行为和外部交互之间也存在一定 的联系，这些联系使得这些松散的模型之间能够彼此联系起来，呈现系统的整体 图画。u m l 在软件工程领域得到了广泛的应用，它准确直观的特点被众多软件设 计者与开发者所喜爱，在很多程序开发平台上都集成了支持u m l 语言的建模界 3 华东师范大学博士学位论文第一章。绪论 面，甚至支持从模型到程序代码的转换，如微软的v i s u a ls t u d i o ，m m 的r a t i o n a l r o s e 等。本文吸收了u m l 建模方法中将系统特征分别建模的思想，使用形式化模 型来描述系统的各个方面，可以在这些模型内部独立研究系统在该方面满足的性 质，而后通过模型组合方式将这些模型组合成符合给定性质的系统模型。 模型检查( m o d e lc h e c k i n g ) 是一种基于模型的软件性质验证技术 2 9 ，2 8 ，1 5 ， 7 2 。该技术将待验证的系统抽象为一个状态变迁模型，将系统性质描述为逻辑公 式。模型检查技术通过对模型的状态空间进行遍历，判定给定性质在状态空间上 是否得到满足。模型检查提供了很多有效的工具支持对软件系统的性质验证，代 表工具有：通用模型检查器s p i n 5 9 】，针对实时系统的模型检查器u p p a a l 1 3 】， 针对c 语言源码的模型检查器c b m c 2 7 ，2 6 ，6 5 等等。 模型驱动的工程( m o d e l d r i v e ne n g i n e e r i n g ) 是软件工程领域中的一种软件 开发方法论 8 6 ，1 2 。它指出软件开发应该针对各种不同领域的模型，用程序语言 描述各种领域相关的概念和活动，使得软件系统能够更加高效的为特定领域的用 户提供服务。对象管理组织( o m g ) 提出了模型驱动的体系结构+ ( m o d e l d r i v e n a r c h i t e c t u r e ) 作为一种软件设计与开发标准【l ，4 2 ，6 4 。模型驱动的软件开发过 程包括：先使用领域语言给出系统的一个平台无关的模型( p l a t f o r m i n d e p e n d e n t m o d e l ) ，再针对不同的运行平台将这个模型依照一定的转换规则转换为一系 列平台相关的模型( p l a t f o r m s p e c i f i cm o d e l s ) 。平台相关的模型可以表示成通用 程序语言j z t l j a v a ，c # 等写成的程序代码，直接被计算机执行，从而完成从抽象 模型到程序代码的软件开发过程。模型驱动的软件开发方法提供了很多支持 将平台无关模型转换为平台相关模型的理论和自动化工具。模型转换( m o d e l t r a n s f o r m a t i o n ) 是模型驱动开发方法中的一个重要组成部分，它依靠一个统一的 元模型( m e t a m o d e l ) ，构造一系列转换规则将一个源模型转换为一个或多个目标 模型。在从抽象模型到程序代码的转换过程中，可能需要经历很多次模型转换过 程。模型转换可以大致分为以下几类【31 ，7 3 】： 内生转换( e n d o g e n e o u st r a n s f o r m a t i o n ) ，源模型和目标模型依赖于同一个元 模型。 外生转换( e x o g e n e o u st r a n s f o r m a t i o n ) ，源模型和目标模型依赖于不同的元 模型。 水平转换( h o r i z o n t a lt r a n s f o r m a t i o n ) ，源模型和目标模型具有相同的抽象层 次。 垂直转换( v e r t i c a lt r a n s f o r m a t i o n ) ，源模型和目标模型具有不同的抽象层 次。 4 第一章绪论华东师范大学博士学位论文 模型转换过程本身也可以被抽象为模型，因此存在相应的高阶模型转换方法，将 描述模型转换的模型本身作为模型转换的源模型或目标模型。模型转换理论被描 述成各种模型转换语言( m o d e lt r a n s f o r m a t i o nl a n g u a g e ) ，帮助实现不同领域模 型的转换过程。f f i j ! z d o m g 提出的q v t 标准【2 】，i n r i a 提出的a t l a s 语言等。 精化演算( r e f i n e m e n tc a l c u l u s ) 是另外一种研究模型转换的理论，它通过逐 步精化的方式将一个系统的抽象行为描述转化为一个正确高效的可执行程序。精 化演算的主要特点是在每一次转换过程中，保持目标模型是源模型的精化，从而 保证源模型满足的性质在目标模型中仍然被满足。r a l p h j o h a nb a c k 教授在他的博 士论文中首次提出了使用精化方法来进行软件开发的思想【1 1 】。c a r r o l lm o r g a n 教 授在他的著作( 、p r o g a m m i n gf r o ms p e c i f i c a t i o n s ) ) 中详细介绍了精化演算方法的过 程【7 9 】。他通过程序精化手段，将使用j e a n r e y m o n da b r i a l 教授提出的z 语言描述 的系统规范转换为可执行的d i j k s t r a s e 式程序，实现了从需求规范到程序代码的完 整软件开发过程。 本文研究的模型组合理论的目的是希望通过模型间的信息共享和协调，从已 有的模型基础上构造出更符合系统需求的模型。其中也涉及到模型之间的转换， 这些转换以模型间能够共享的信息为基础，使不同模型中的信息能够相互共享和 补充，并在组合过程中使组合模型保持原模型中已经满足的良好性质。模型组合 与模型转换的主要区别是关注点不同，模型转换主要是在统一的元模型描述基础 上进行从平台无关模型到平台相关模型的转换，程序精化演算也主要关注从抽象 模型到具体模型的自上而下的纵向精化过程。而模型组合旨在将不同建模方式下 的模型信息进行横向整合，补充和完善模型对系统的描述，从多个对系统不同特 征进行描述的局部模型过渡到对系统性质进行全面研究的整体模型。 目前，对模型进行横向组合的研究才刚刚起步，还未形成统一的研究方法和 理论。很多研究小组针对具体的模型组合场景提出了将一些特殊模型进行组合的 方法，取得了初步的成果。这些使用组合模型的理论方法已经逐渐向工程应用领 域转化。典型的研究成果包括： 将描述程序规范的z 方法与描述程序间通信的c s p 方法进行组合，构造一种 兼容了这两种方法的全新模型，能够对系统的数据状态变迁和通信行为进行 统一的解释。代表成果有c s p z 1 4 ，1 0 0 】，c s p o z 4 0 等。 将描述程序状态机的b 模型与描述程序间通信的c s p 模型进行组合，使 用c s p 通信动作序列对b 状态机进行约束，同时使用两种模型对系统行为进 行刻画。代表成果有c s pj j b 1 9 ，8 8 ，7 0 ，7 1 等。 将描述状态的z 语言、描述事件的c s p 语言与描述时间性质的d c 语言结合起 5 华东师范大学博士学位论文第一章绪论 来，使用程序统一理论对以上模型建立统一的语义模型，并在该模型基础上 讨论系统性质。代表成果有c i r c u s 9 9 ，1 0 1 ，8 2 ，8 1 等。 与上述研究工作相比，本文重点研究模型组合过程，旨在提出组合的一般手段， 研究满足一定条件的模型通过不同组合方式所得到的组合模型具有何种性质，而 不针对具体的模型组合场景研究组合模型的具体应用。 1 2 程序统一理论 程序统一理论u t p ( u n i f y i n gt h e o r i e so fp r o g r a m m i n g ) 由图灵奖获得者t 0 n v h o a r e 与中科院院士何积丰于1 9 9 8 年创立【5 4 。程序统一理论是一套典型的形式化 方法，它涉及程序基础理论的诸多领域，为程序语言提供了一个一致的理论基础。 程序统一理论考察了各种程序语言在程序风范、抽象层次、表现形式等方面的不 一致问题，旨在发现一个能够解释不同程序理论的清晰一致并具有说服力的统一 方法。 程序统一理论的出发点是能够在计算机科学领域找到与现代数学和物理学类 似的清晰优美的理论框架与体系结构。这个理论首先应当包含一个具有说服力 的方法，指出计算机程序语言的应用范围，同时还需要引入一些在所有程序语言 领域都会涉及到的基本的概念和性质。另外，它需要能够处理一些针对某些特殊 的程序语言特性而产生的程序语言的扩展或变化过程。这个理论的结构应该具 有可组合的特性，即复杂结构的属性能够通过简单的相互独立的基本元素的属 性构造出来。另一方面，一个实际的程序语言包含了大量的属性，并且需要在实 现的高效性和程序的兼容性之间做出一些折中，而这些折中方案往往没有统一 的理论方法来进行指导和规范。现有的程序语言种类繁多，根据他们的计算风范 ( c o m p u t a t i o np a r a d i g m ) 进行初步分类后，每个程序语言的抽象层次也很不一致。 因此，为当前流行的各种程序语言构造一个有效的概念框架一直是程序理论研究 者所面临的挑战。而程序统一理论就旨在应对这样的挑战。 何积丰院士及其研究小组已经利用程序统一理论对各个领域具有各种不同 特征的程序语言进行了研究，其中包括经典的描述串行程序性质的d i j k s t r a 语言， 描述进程间通信性质的a c p 语言，c s p 语言，用于面向对象程序设计的r c o s 语 言 4 9 】，用于软硬件协同设计的v e r i l o g 语言 1 0 2 ，1 0 3 】，描述w e b h 艮务组合的b p e l 语 言 5 1 】，w e b 事务处理语言【6 8 等等。统一程序语言在这些程序语言研究中的应用 使我们相信，目前大多数程序语言所关注的程序行为方面的性质，都能够在该理 论框架下进行统一的描写和系统的研究。此外，u t p 方法还被用来描述很多基于 网络环境和服务架构的软件系统，为这些系统建立了形式化模型，并支持分析和 6 第一章绪论 华东师范大学博士学位论文 验证系统的性质 4 7 ，2 3 。 1 2 1 基于字母表的程序理论 程序统一理论引入一个字母表( a l p h a b e t ) 的概念来描述程序理论中的基本 概念与物理世界的观察和实验的关联。在字母表的基础上选择一些符号来表示理 论的基本原语以及把这些原语连接成更加复杂的语句的方法，这些符号被称为理 论的特征集( s i g n a t u r e ) 。最后，理论所得出的结论( l a w ) 被表示成一系列能够 进行数学证明的等式或不等式，他们有助于程序的设计和对程序执行结果的预测。 程序统一理论认为字母表、特征集和结论是一个理论的核心组成部分。不同理论 的相容之处在于他们在这三个部分上有相同的组成元素；他们的差异也体现在这 三个部分的差异上。 与其他的自然科学理论一样，程序理论可以使用观测到的程序行为所满足的 等式、不等式或其他数学关系来表示。这种表示可以通过以集合论和逻辑为基础 的数学手段来实现。集合论与逻辑中往往包含一些自由变量，用来表示理论中某 些观测的可能结果，当这些观测结果确定之后，有意义的结论就产生了。这些观 测的含义和进行观测的方法往往基于特定领域的共识，且根据领域的不同对观测 量的选择也存在很大差异。在程序统一理论中，使用谓词来表示理论中的结论， 采用字母表来给理论中所选择的每个观测量一个确定的名称，且在所有理论中对 同一个观测量使用同一个名称。字母表的确定是建立和研究程序理论的重中之重， 它确定了对程序行为的观察范围，决定了该程序理论能够描述程序行为的哪些特 征。 通常，对一个程序的执行行为的一种表示是在程序执行前后其所使用的数据 变量值的变化关系。在字母表中，一般使用z y ，z 来表示在程序执行前对具有这些 名称的数据变量的状态值的观察，用z 7 y 7 z i 表示在程序执行之后对这些数据变量 的状态值的观察。这时，程序理论就是描述程序执行前后，其数据变量值的变化 所满足的性质。另外，对于一些简单的程序理论中所涉及的关于程序启动与终止 状态的描述，字母表中使用两个布尔类型的变量d 后，o 七7 分别表示对程序的启动与 终止状态的观察。一些具有反应性质( r e a c t i v e ) 的程序理论还需要描述程序的等 待行为，即程序执行中处于稳定的中间态，直到特定条件成立时才产生响应。为 了表示这种观测结果，反应程序理论的字母表中需要引入布尔变量w a i t ，当它为 真时，表示程序处于等待状态。在一些关注程序间通信协议的程序理论中，还需 要在字母表中引入一个动作序列来记录程序间产生的通信，以便于描述这些通信 在时间上的先后顺序。 通过以上的例子我们发现，若某一理论关注程序的某个行为特征，我们需要 7 华东师范大学博士学位论文第一章绪论 在该理论的字母表中引入相应的变量来表示这些行为所依赖的物理观察。每个理 论都有一个有限的确定的字母表，字母表中未涉及的观测结果无法在该理论中进 行描述。换言之，一个理论只选择程序的某些行为特征进行研究，不涉及任何其 他的行为特征。若某些理论的字母表共享某些变量，那么这些理论都具有对程序 这些方面的特征的描述能力，根据程序统一理论，这些理论对这些特征的描述应 当是一致的。 程序统一理论中提出了一种称为d e s i g n 的程序理论。d e s i g n 理论的字母表 中包含对程序执行前后的数据状态的观察z ，z 7 以及对程序启动与终止状态的观 察d 七，d 七7 ，程序的执行行为或描述程序行为的规范被统一表示成作用在字母表上 的一阶谓词。具体而言，一个程序p 在d e s i g n 理论中被表示成 p = d ro kab ( x ) 令o k 7an ( x ，z 7 ) 其含义为程序尸正常启动，并且初始数据状态满足b ，那么p 能够正常终止，且最 终数据状态与初始数据状态满足r 。d e s i g n 理论精确的表示了程序在数据状态和终 止情况这两个观察结果上的行为。 在此基础上，d e s i g n 理论进一步定义了经典的d i j k s t r a 语言中的各种程序组 合算子，包括串行组合、条件选择、非确定选择、循环等，并证明这些算子关 于d e s i g n 空间是封闭的，即在这些组合算子的作用下，组合程序仍然具有d e s i g n 的 形式与性质，从而保证了程序的可组合性。 1 2 2 程序理论的联接 联接理论( l i n k i n gt h e o r y ) 是程序统一理论中的重要组成部分。该理论讨论 了共享符号集的理论之间应该满足的关系。这种联接关系集中表现为理论之间共 享的符号在各自的理论空间中保持相类似的含义。程序统一理论主要讨论了两种 理论之间的联接，一种被称为子集理论，另一种被称为g a l o i s 连接 3 8 ，1 0 ，程序 统一理论讨论了具有这两种联接关系的理论中的对象和符号的语义之间如何相互 联系、相互转化。 在子集理论中，一个理论的表示空间丁是另一个理论s 的子集。这时，我们需 要保证在s 和丁共同的符号集上的运算具有相同的含义且该运算在