（计算机系统结构专业论文）基于进程代数的面向服务软件体系结构建模.pdf

? 1 i 女麓， i + f ， ，0 p ， 、 at h e s i sf o rt h ed e g r e eo fm a s t e ri nc o m p u t e r a p p l i c a t i o nt e c h n o l o g y m o d e l i n gs e r v i c e - - o r i e n t e da r c h i t e c t u r eb a s e do np r o c e s s a l g e b r a b yl ih u i s u p e r v i s o r ：p r o f e s s o rq i a oj i a n z h o n g n o r t h e a s t e r nu n i v e r s i t y j u n e2 0 0 8 i j i y 划 ，一 ， 。” f - 独创性声明 本人声明所呈交的学位论文是在导师的指导下完成的。论文中取得的 研究成果除加以标注和致谢的地方外，不包含其他人已经发表或撰写过的 研究成果，也不包括本人为获得其他学位而使用过的材料。与我一同工作 的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示诚挚 的谢意。 学位论文作者签名：方笔 签字e l 期：砀c 7 ，万 学位论文版权使用授权书 本学位论文作者和指导教师完全了解东北大学有关保留、使用学位论 文的规定：即学校有权保留并向国家有关部门或机构送交论文的复印件和 磁盘，允许论文被查阅和借阅。本人同意东北大学可以将学位论文的全部 或部分内容编入有关数据库进行检索、交流。 含作者和导师同意网上交流的时间为作者获得学位后： j 。y f p 半年口一年口一年半口两年口 学位论文作者签名：疹笔、 签字日期： 导师签名： 签字日期： i j i l ， 、 嘈q r l ， “ 东北大学硕士学位论文摘要 基于进程代数的面向服务软件体系结构建模 摘要 随着软件技术的发展，一种被称为面向服务软件体系结构s o a 的软件系统开发方 法被提出并得到迅速发展。今天的s o a 是基于已经广泛接受的w e b 服务标准，被誉为 下一代w e b 服务的基础框架。但是目前大多数对s o a 的研究仍集中在w e b 服务标准的 拓展、w e b 服务开发工具以及服务应用集成等方面，对s o a 系统架构设计和形式化建 模方面的研究还缺乏关注。本文采用一种基于p i 演算的描述语言z r a d l ，对s o a 系统 的形式化建模过程进行详细的描述和验证。 论文首先对面向服务的相关技术和p i 演算基本理论进行阐述。在此基础上给出了 服务的相关定义和服务模型，描述了服务的角色、元素、服务属性以及服务之间的交互 关系。利用p i 演算对服务、角色以及操作进行定义，以及对服务属性进行详细的描述 和分析。 本文采用基于移动进程理论p i 演算的描述语言，r a d l 对s o a 模型进行形式化规 约，为s o a 的应用和系统设计提供形式化的描述、分析和验证方法。首先介绍s o a 架 构的基本结构，包括服务、连接件、系统配置等，然后用刀 a d l 直接、显式地对这三部 分进行规约。服务是具有统一描述性的组件集合，万a d l 通过对端口、角色进行规约， 从而独立地描述组件、连接件的功能行为。系统配置是服务、连接件按照特定方式组织 而成的有机整体，主要研究组件或服务的组装，其中组件组装成服务，服务也可以组装 形成组合服务。组装技术包括端口组装、连接件连接以及组装运算操作。 论文最后介绍了一个简单s o a 系统的建模实例，用专门针对p i 演算开发的自动验 证工具移动工作台m w b ( m o b i l i t yw o r k b e n c h ) 来验证s o a 模型分析和建模过程的正 确性。 关键词：进程代数；面向服务软件体系结构；p i 演算；，r a d l ；组合服务 i i 、 、： ， 东北大学硕士学位论文 a b s t r a c t m o d e l i n gs e r v i c e - o r i e n t e da r c h i t e c t u r eb a s e d o np r o c e s s a l g e b r a a bs t r a c t w i t ht h ed e v e l o p m e n to fs o f t w a r et e c h n o l o g y , ad e v e l o p i n gm e t h o do fs o f t w a r es y s t e m w h i c hi sn a m e ds e r v i c e - o r i e n t e da r c h i t e c t u r ei sp r e s e n t e da n dd e v e l o p sr a p i d l y n o w d a y s ， s o ai sb a s e do nc r i t e r i o no fw e bs e r v i c e sw h i c hh a sb e e na c c e p t e dw i d e l y , i ti sc o n s i d e r e da s b a s i cf r a m eo fn e x tg e n e r a t i o n a lw e bs e r v i c e s a c c o r d i n gt ot h a tt h er e s e a r c h e so nw e b s e r v i c e sa r em o s t l yf o c u s i n go nt h es t a n d a r de x t e n s i o n ，d e v e l o p i n gt o o l sa n di n t e r g r a t i o n a p p l i c a t i o n s ，t h ed e s i g nm e t h o d sa n df o r m a l i z e dm o d e l i n go fs o as y s t e mh a ss h o w e dm a n y i n s u f f i c i e n c i e s w ea d o p tn ra d lt od e s c r i b et h ep r o c e s so ff o r m a l i z e dm o d e l i n go fs o a s y s t e ma n d v a l i d a t ei t f i r s t l y , t h i st h e s i si n t r o d u c e sc o r r e l a t i v et e c h n o l o g yo fs e r v i c e - o r i e n t e da n dt h et h e o r y o fp ic a l c u l u s s e c o n d l y , i tp r e s e n t ss e r v i c ed e f i n i t i o na n dm o d e l ，a n dd e s c r i b e st h es e r v i c e r o l e s ，e l e m e n t s ，a t t r i b u t e sa n di n t e r a c t i o n s a tl a s t ，s e r v i c e ，r o l e s ，a n do p e r a t i o n sa r ed e f i n e d b y t h ep ic a l c u l u s ，a n ds e r v i c ea t t r i b u t e sa r ec o m p r e h e n s i v e l yd e s c r i b e da n da n a l y z e d f o rp r o v i d i n gt h ef o r m a l i z a t i o nm e t h o d st o d e s c r i b e ，a n a l y z ea n dv a l i d a t e t h e a p p l i c a t i o n sa n dd e s i g no fs o a ，t h i st h e s i sp r e s e n t st h ef o r m a l i z a t i o ns t i p u l a t i o n so fa n a g r e e m e n to fs o am o d e l i n gu s i n gt h e 7 ra d l ，w h i c hi sb a s e do nm o b i l ep r o c e s st h e o r yp i c a l c u l u s a tf i r s t ，a u t h o rp u t sf o r w a r dt ob a s i cs t r u c t u r eo fs o a ，i n c l u d i n gt h es e r v i c e ， c o n n e c t o ra n dc o n f i g u r a t i o n ，t h e np r e s e n t ss t i p u l a t i o n so fa na g r e e m e n to ft h e m s e r v i c ei s g a t h e r e db yt h ec o m p o n e n t sw h i c ha r ed e s c r i b e du n i f o r m l y n a d l d e s c r i b e st h eb e h a v i o ro f c o m p o n e n t sa n dc o n e c t o r si n d e p e n d e n t l yb yc a r r y i n gs t i p u l a t i o n so fa na g r e e m e n to fp o r t s a n dr o l e s c o n f i g u r a t i o no fs o ai sa no r g a n i s mt oa s s e m b l et h ec o m p o n e n t so rs e r v i c e si na s p e c i a lw a y c o m p o n e n t sc o u l d b ea s s e m b l e dt os e r v i c e st h e ns e r v i c e sc o u l db ea s s e m b l e dt o c o m p o s i t es e r v i c e s t h et e c h n o l o g yo fa s s e m b l i n gi n c l u d e sa s s e m b l i n gp o r t s ，c o n n e c t o r sj o i n a n da s s e m b l i n go p e r a t i o n s a tl a s t ，t h i sp a p e ri n t r o d u c e sa ne x a m p l eo fs o a m o d e l i n g ，a n dv a l i d a t e st h ep r o c e s so f m o d e l i n ga n da n a l y s i sb ym w b ，w h i c hi sat o o lt ov a l i d a t ea u t o m a t i c a l l ya n db a s e do np i 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 ；s o a ；p ic a l c u l u s ；n - a d l ；c o m p o s i t es e r v i c e s i i i 、 、 东北大学硕士学位论文目录 目录 独创性声明i 摘要i i a b s t r a c t i i i 第1 章引言1 1 1 研究背景和意义。l 1 2 研究现状和问题。1 1 3 本文主要研究内容3 1 4 本文组织结构4 第2 章研究基础5 2 1 软件体系结构5 2 1 1 软件体系结构定义一5 2 1 2 体系结构形式化方法和描述语言6 2 2 服务相关技术8 2 2 1 组件9 2 2 2 可扩展标记语言( l ) 9 2 2 3w | e b 服务1 0 2 3 面向服务的软件体系结构( s o a ) 1 2 2 3 1s o a 定义1 2 2 3 2s o a 基本特征及优点1 3 2 4 小结一1 4 第3 章p i 演算基本理论1 5 3 1 引言一15 3 2p i 演算的基本语法1 6 3 2 1 名字与进程1 6 3 2 2 自由与约束的名字。1 7 3 3p i 演算的标签操作语义1 8 3 4p i 演算的行为等价规则2 0 3 4 1 强互模拟和弱互模拟一2 0 3 4 2 迟互模拟和早互模拟2 2 3 4 3 闭互模拟和开互模拟。2 3 3 5 小结一2 4 第4 章基于p i 演算的服务建模及属性描述2 5 4 1 服务建模2 5 一 东北大学硕士学位论文 目录 4 1 1 服务定义2 5 4 1 2 服务模型2 6 4 2p i 演算描述服务以及服务模型3 1 4 2 1p i 演算描述服务3 2 4 2 2p i 演算描述服务属性3 3 v 4 3 小结3 8 第5 章基于p i 演算的s o a 建模研究3 9 5 1s o a 参考模型3 9 5 1 1 概述3 9 5 1 2s o a - 刚的组织结构4 0 5 1 3s o a r m 的层次结构4 1 5 2 基于p i 演算的s o a 建模4 2 5 2 1s o a 基本结构4 2 5 2 2 万a d l 描述s o a 模型结构4 3 5 2 3 服务( s e r v i c e ) 规约4 3 5 2 4 连接件( c o n n e c t o r ) 规约4 6 5 2 5 配置( c o n f i g u r a t i o n ) 规约4 8 5 3s o a 建模分析5 5 5 4 小结。5 8 第6 章s o a 系统模型实例的分析与验证5 9 6 1s o a 模型实例研究5 9 6 2s o a 模型分析与验证6 5 6 2 1 移动工作台m w b 6 5 6 2 2s o a 系统实例的模型输入6 6 6 2 3 实例模型的分析与验证6 7 6 3d 、结。6 8 第7 章总结6 9 7 1 论文内容总结6 9 7 2 将来的研究工作6 9 参考文献7 1 致谢。7 5 一v 一 东北大学硕士学位论文第1 章引言 第1 章引言 1 1 研究背景和意义 随着i t 产业的迅速发展，软件系统的规模越来越大，复杂度也越来越高，软件技 术也在不断变化以适应企业的发展。从早期的结构程序设计方法到面向对象的程序设计 方法，从非形式化的软件体系结构到形式化的软件体系结构方法。后来出现了服务的概 念【l 】，服务的复用性和交互性使服务可以轻易地重组，以适应当前复杂业务流程的变化。 因此，服务及其相关技术就成为当前i t 界的焦点技术，把服务流水化作业的思想引入 到软件开发当中，就形成了s o a ( s e r v i c e o r i e n t e d a r c h i t e c t u r e ，面向服务的体系结构) 的理念【2 1 。 面向服务的体系结构s o a 是未来的发展趋势，g a r t n e rg r o u p 预测到2 0 0 8 年，s o a 将成为占绝对优势的软件工程技术。采用s o a 架构可以快速、灵活的应对信息系统的 调整需求。而传统的系统架构和编码方式在应对企业新需求时，往往存在调整周期长、 费用高、重用率低等不足之处，使得系统的需求调整很难得到快速实施。同时，传统的 开发模式是通过打补丁、版本升级等方式来满足需求的变化，导致了后来的版本混乱， 软件系统过于繁杂。s o a 是软件领域别开生面的技术，它借用了服务业和建筑业的核心 思想，与经典的分布式及组件原理相结合，形成了软件技术一座新的里程碑。s o a 具有 灵活性、可扩展性等优秀属性，使服务之间能够容易地根据复杂多变的业务流程不断重 组。其松耦合、服务导向的架构思想，给i t 系统的实施者们描绘了一个快速开发、随 需而变的美好前景。 随着s o a 系统的广泛应用，系统建模的描述以及验证成为一个重要的问题。非形 式化的软件开发方法，给软件系统的开发带来了诸多的困难，描述不明确、不一致，导 致设计、编成的错误，甚至繁重的修改，造成软件系统可靠性差，开发价格昂贵。形式 化方法是建立在严格数学基础上，采用严格的数学工具、具有精确数学语义的软件开发 方法。它具有明确性、一致性和完整性等特点，能很好地对软件系统进行描述和验证， 使系统具有良好的结构、易维护、能较好地满足用户需求，助于增加软件开发人员对软 件系统的理解，保证程序的正确性，将极大增强软件开发的可靠性。 1 2 研究现状和问题 东北大学硕士学位论文 第1 章引言 2 0 世纪6 0 年代开始，由于软件成本日益增大，软件开发进度难以控制，软件质量 差和软件维护困难，软件危机的程度日益加剧，重点放在数据结构和算法选择上的软件 工程方法，对于大规模、复杂化的软件系统，显得力不从心。人们面临的问题不仅仅是 考虑软件系统的功能问题，还要解决更难处理的非功能性要求，如系统的性能、可适应 性、可重用性及可靠性等，使得总体的系统结构设计和规格说明成为软件设计的核心， 人们开始注重软件体系结构的研究。尤其是在2 0 世纪9 0 年代后期，众多学者借鉴计算 机体系结构和网络体系结构中先进的思想和方法，使得软件体系结构的研究已完全独立 于软件工程的研究，成为计算机科学的一个新的研究方向和独立学科分支。 关于软件体系结构，目前还没有统一的、标准的定义。许多专家学者从不同的角度、 不同的侧面对软件体系结构进行了定义，比较有影响的有d e w a y n ep e r r y 和a l e xw o l f , m a r ys h a w 和d a v i dg a r l a n 等【3 一钉。国内对于软件体系结构的研究尚处在起步阶段，虽 然有些有关软件体系结构方面的文章，多是与特定应用有关。主要包括体系结构风格、 体系结构规约、体系结构模型等。体系结构风格可以分类为数据流风格、调用返回风格、 独立构件风格、虚拟机风格、仓库风格等。体系结构规约又分为两类：体系结构形式化 方法和体系结构描述语言。 在软件体系结构描述方面，早期主要是采用图和文本等非形式化的描述方法，如流 程图、决策树和甘特图等，难以被开发人员理解及进行分析和模拟。为了克服非形式化 方法对于开发软件系统所带来的问题，人们越来越注重软件体系结构形式化方法的研 究，采用形式化方法、形式化语言来描述软件体系结构。形式化方法主要有一阶谓词演 算、基于逻辑、状态机、网络、进程代数【5 1 、 p e t r i 网【6 】；形式化描述语言有如o b j 、时 序逻辑、z 语言、c s p 、c c s 、p i 演算【7 1 。随着软件研究与应用的发展，出现了很多体 系结构描述语言a d l s ，比如，a e s o p 、c 2 、d a r w i n 、r a p i d e 、s a d l 、u n i c o n 和w r i g h t 等，尽管它们都描述软件体系结构，却有不同的特点。这些a d l 强调了体系结构不同 的侧面，对体系结构的研究和应用起到了重要的作用。 面向服务的体系结构s o a 思想，最早由g a r t n e r 于1 9 9 6 年提出，g a r t n e r 为s o a 描 述的远景目标是：让i t 变得更有弹性，以更快地响应业务单位的需求，实现实时企业 ( r e a l t i m ee n t e r p r i s e ) 。他预测到2 0 0 8 年，8 0 的客户将使用s o a 用于新产品开发。 因此，到2 0 0 8 年的这段时间，都将是s o a 引擎平台的建设过程。目前国外已有基于 s o a 的很多成功案例，包括金融、证券、医药等领域，而在国内，基于s o a 的应用还 属于起步阶段，但已有相当数量的企业在相应范围内开始逐步实施。面向服务的架构 一2 -一厶- 东北大学硕士学位论文第1 章引言 ( s o a ) 是每个企业都想努力实现的一个架构。由于s o a 集合了w e b 服务等基于行业 标准的软件组件，能让企业建立灵活的、可重复使用的应用关联来应对特定的行业问题。 而且s o a 把业务组件分成基本的构建模块，就像通过标准化软件接口实现b c 基础设 施的模块化，从而使灵活的业务流程可以与灵活的b c 流程相匹配。然而，实现s o a 的道路不是那么平坦，要实现架构承诺的目标具有一定难度。但随着各企业和系统集成 商的投入和研究，最终实现s o a 是完全可能的。 s o a 是一种用于构建分布式系统的方法，采用s o a 这种方法构建的分布式应用程 序可以将各功能模块作为服务交付给终端用户，也可以用它来构建其他的服务。面向服 务的体系结构s o a 可以基于w e b 服务，但是它可能由其他的技术来代替。在使用面向 服务的体系结构( s o a ) 设计分布式应用程序时，可以将w e b 服务的使用从简单的客 户端朋艮务器( c l i e n t s e r v i c e ) 模型扩展成任意复杂的系统。 目前针对面向服务的软件体系结构的研究，主要有两个方面：服务的研究以及s o a 参考模型和架构平台的研究。首先，大部分的研究是针对服务的，研究服务的定义、角 色、交互关系以及服务的相关技术。比如为了研究服务，人们引入了形式化的方法， r a c h i dh a m a d i 提出了基于p e t r i 网的服务组合模型；澳大利亚q u e e n s l a n du n i v e r s i t yo f t e c h n o l o g y ( q u t ) 的业务流程管理研究组用p e t r i 网建立了不同的语义模型。其次，是对 s o a 参考模型以及具体实施s o a 架构的实现平台( w 曲服务) 进行研究。比如，o a s i s 给出了s o a 的参考模型【8 】；w 3 c 也有它们自己的基于w e b 服务的服务框架；作为几个 i t 巨头之一i b m 同样在红皮书系列中分析了s o a 中服务模式【9 】；i o n a 公司首席技术 官e r i cn e w c o m e r 提出的用w e bs e r v i c e s 对s o a 进行建模【1 0 】。 然而很少有文章对服务属性有深入的描述，对s o a 的建模过程理解的不是很透彻。 在面向服务的软件体系结构形式化描述方面，相关的研究成果较少，目前还没有一个较 好的描述方法。 1 3 本文主要研究内容 本文以基于移动进程理论p i 演算吲作为形式化理论基础，结合软件体系结构理论、 方法和面向服务的体系结构内涵，用基于p i 演算的面向服务软件体系结构形式化描述 语言n a d l 1 1 1 描述s o a 模型，旨在为面向服务的体系结构应用和系统设计提供形式化 的描述、分析和验证方法，加深对s o a 技术的理解，提高系统分析、设计的明确性、 一致性和准确性。最后再用专门针对p i 演算开发的自动验证工具移动工作台m w b 一3 一 东北大学硕士学位论文第1 章引言 ( m o b i l i t y w o r k b e n c h ) 【1 2 】来验证s o a 模型建模过程的正确性。主要研究内容如下： ( 1 ) 对以前的一些基础理论进行综述，如软件体系结构、面向服务的相关技术、 s o a 概念以及p i 演算的一些基本理论。 ( 2 ) 给出服务的相关定义，对服务进行分析从而建立服务模型；然后再描述服务的 角色、元素、服务属性以及服务之间的交互关系；最后用p i 演算定义了服务、服务角 色以及服务操作，并对服务属性进行详细的描述和分析。 ( 3 ) 简单介绍s o a 参考模型的概念，分析了s o a 参考模型的组织结构和层次结构， 再用基于p i 演算的n r a d l 对s o a 模型进行建模，分别从服务规约、连接件规约和配置 规约三个方面对建模过程进行描述，之后再介绍了一些s o a 模型的分析技术。 ( 4 ) 对一个简单的服务系统进行s o a 建模，然后把各个模型的进程表达式输入 m w b 工具中，并用工具命令对s o a 模型实例进行分析和验证，从而证明文章前面部分 的建模方法和分析技术是正确可行的。 1 4 本文组织结构 论文内容分为七章。 第一章是引言，总领全文。第二章是研究基础，首先给出软件体系结构的知识，然 后再介绍面向服务的相关技术以及面向服务的软件体系结构s o a 的基础知识。 第三章简要介绍p i 演算的基本理论，是后续研究工作的理论基础。 第四章基于p i 演算的服务建模及属性描述，先给出服务的定义，对服务进行分析 从而建立服务模型，然后具体阐述了服务的元素、角色、属性以及服务之间的交互关系， 最后用p i 演算定义服务、服务角色以及服务运算操作，并详细描述服务的一些基本属 性。 第五章是基于p i 演算的s o a 建模研究。先简单介绍了s o a 参考模型的概念，给 出s o a 参考模型的组织结构和层次结构，然后再用基于p i 演算的描述语言n r a d l 从服 务规约、连接件规约以及配置规约三个方面详细描述s o a 模型的建模过程。最后再介 绍了一些s o a 模型的分析和验证技术。 第六章是s o a 系统模型实例的分析和验证。对一个简单的服务系统进行s o a 建模， 然后把各个模型的进程表达式输入m w b 工具中，并用工具命令对s o a 模型实例进行 分析和验证。 第七章是全文总结和研究工作展望。 4 东北大学硕士学位论文第2 章研究基础 第2 章研究基础 本章主要对国内外一些相关基础理论研究做一综述。首先简单介绍软件体系结构定 义，阐述了一些体系结构的形式化方法和体系结构描述语言。然后给出面向服务的一些 相关技术，比如组件技术、x m l 以及w e b 服务技术。最后再介绍了面向服务的软件体 系结构的定义，并详细介绍s o a 的基本特征以及优势等。 2 1 软件体系结构 六十年代的软件危机使得人们开始重视软件工程的研究。起初，人们把软件设计的 重点放在数据结构和算法的选择上，随着软件系统规模越来越大、越来越复杂，整个系 统的结构和规格说明显得越来越重要。软件危机的程度日益加剧，现有的软件工程方法 对此显得力不从心。对于大规模的复杂软件系统来说，对总体的系统结构设计和规格说 明比起对计算的算法和数据结构的选择已经变得重要得多。在此种背景下，人们认识到 软件体系结构的重要性，并认为对软件体系结构的系统、深入的研究将会成为提高软件 生产率和解决软件维护问题的新的最有希望的途径。 2 1 1 软件体系结构定义 关于软件体系结构的定义，有许多学者曾从不同角度和不同侧面给出过一些定义， 比如，d e w a y n ep e r r y 和a l e xw o l f 定义软件体系结构是具有一定形式的结构化元素， 即组件的集合，包括处理组件、数据组件和连接组件【4 】；m a r ys h a w 和d a v i dg a r l a n 认 为软件体系结构是软件设计过程中的一个层次，这一层次超越计算过程中的算法设计和 数据结构设计【3 1 ；k r u c h t e n 认为软件体系结构有四个角度，它们从不同方面对系统进行 描述：概念角度、模块角度、运行角度、代码角度：d a v i dg a r l a n 和d e w n ep e r r y 认为 软件体系结构是一个程序系统各组件的结构、它们之间的相互关系以及进行设计的原则 和随时间进化的指导方针。 迄今为止，软件体系结构还没有统一的定义，但一般认为它是具有一定形式的结构 化元素，即组件集合，包括处理组件、数据组件以及连接组件。处理组件对数据进行加 工，数据组件是被n - r 的信息，连接组件是用来把体系结构的不同部分组合连接起来的。 软件体系结构的研究主要包括体系结构风格、体系结构规约、体系结构模型等，其 中体系结构风格一般包括以下几种：数据流风格、调用返回风格、独立组件风格、虚拟 一5 _ 东北大学硕士学位论文 第2 章研究基础 机风格以及仓库风格，具体表现为管道过虑器型、面向对象型、层次型、黑板型、状态 变换型、客户j j 艮务器型、p 2 p 型、g e n v o c a 和c 2 型等。体系结构规约又分为两类：体 系结构形式化方法和体系结构描述语言。 2 1 2 体系结构形式化方法和描述语言 ( 1 ) 软件体系结构形式化方法 形式化方法的主要研究内容包括：形式化规格说明( f o r m a ls p e c i f i c a t i o n ) 和形式化 验证( f o r m a lv e r i f i c a t i o n ) 。形式化规格说明一般是用形式化描述语言，如o b j 、时序逻 辑、z 语言、c s p 、c c s 、p i 演算等。形式化验证方法包括模拟( s i m u l a t i o n ) 和测试( t e s t i n g ) ， 它们都是通过实验的方法对系统进行查错。 软件体系结构形式化方法是指直接运用通用的形式化方法来准确描述软件体系结 构，主要目的是克服自然语言、图表等非形式化方法描述体系结构存在的不足。主要有 如下几种形式化方法【1 3 】：基于c h a m 的体系结构形式规约、基于z 语言的体系结构形 式规约、基于一阶逻辑的体系结构形式规约以及基于图论的体系结构形式规约。 基于c h a m 的体系结构形式规约是由i n v e r a r d i 和w o l f 提出的【1 4 】，他们运用化学抽 象机c h a m ( c h e m i c a la b s t r a c tm a c h i n e ) 【1 5 】模型描述软件体系结构，对体系结构的部 分行为属性进行形式化或半形式化证明。但它也存在不足，例如没有提供描述体系结构 的通用方法，不能描述体系结构风格，没有提供系统配置的一致性和完整性分析机制【1 6 1 。 基于z 语言的体系结构形式规约是a b o w d 1 7 1 提出的，它应用z 语言描述体系结构 风格的通用框架，包括体系结构风格的语法域、语义模型以及语法域到语义模型的映射。 但它缺乏统一的语义模型，难于开发，不能方便地对某一单独系统进行规约和分析。 基于一阶逻辑的体系结构形式规约是m o r i c o n i 、q i a n i s 】提出的，它采用一阶逻辑形 式化描述体系结构和体系结构风格，运用一阶逻辑理论描述构、连接件和系统配置。但 它同样缺乏统一的语法和语义模型，不能支持复用，开发难度大，并且要求构件、连接 件、配置、风格等必须用完备的逻辑理论定义，限制了它的应用【l 9 1 。 基于图论的体系结构形式规约是由m u r p h y l 2 0 】提出的，它运用基于图论的技术描述 软件体系结构，研究不同体系结构规约之间的关系。它侧重于研究体系结构之间的关系， 仅仅运用图结构表达系统结构，不能提供系统化的体系结构建模方法【1 6 】。 ( 2 ) 软件体系结构描述语言 软件体系结构描述语言是针对软件体系结构的整体性和抽象特点，参考传统程序设 6 东北大学硕士学位论文第2 章研究基础 计语言，重新设计和开发的形式化语言。它定义和确定了适合软件体系结构表达和描述 的有关抽象元素，为软件系统的概念体系结构建模提供了具体语法和概念框架。 到目前为止，已经有众多学者提出了许多体系结构描述语言，主要有a e s o p 、d a r w i n 、 c 2 、u n i c o n 、r a p i d e 、w r i g h t 等。这些a d l s 通常用交互组件的体系结构配置来描述软 件系统结构的层次化配置。它们直接提供了相应的符号和标记方法，给出体系结构规约 的统一框架，用来规范体系结构的基本元素。因此，它不存在上面所述体系结构形式化 方法的缺点。但是，当前的a d l s 也存在着一些缺点，不能有效支持体系结构风格的规 约、缺少基本的体系结构形式化分析技术、对体系结构组件交互的描述能力不足【1 3 】。下 面将介绍一下各种描述语言的特点以及不足之处。 a e s o p 是d a v i dg a r l a n 等研发的一种体系结构描述语言，也是体系结构设计环境【2 1 1 。 它是应用面向对象的类型框架对体系结构进行描述，应用类定义体系结构的基本元素， 用它们的子类定义体系结构风格的基本术语，运用相互连接的对象来描述软件配置。因 此它提供了软件体系结构的风格实现、分析和约束检测的系列工具。但是它并没有给出 体系结构风格描述的特定机制以及定义他们的相关语义。 d a r w i n 是m a g e e 和k a r m e r 等开发的一种体系结构描述语言【2 2 1 。它通过接口描述了 组件类型，系统配置则描述组件实例化声明，并在请求服务接口和提供服务接口之间建 立绑定。d a r w i n 通过p i 演算提供了系统结构规约的语义，它支持体系结构的动态演化。 虽然如此，d a r w i n 还是存在着一定的不足【2 3 1 ，它没有提供任何方法和技术描述组件及 服务的性质，因此没有提出一个合适的理论基础去分析体系结构的行为。此外，d a r w i n 中没有提出显式连接件的概念，在需要定义体系结构风格的时候，它不能定义交互模型， 只能支持非对称的交互模式，不能有效描述体系结构规约。 c 2 是r i c h a r dn t a y l o r 等开发的一种体系结构描述语言【2 4 1 。c 2 是基于消息的，它 的组件模型包括上下两端，即消息的发送和接收端口。它用消息总线做为连接机制，用 以对消息进行过滤和转发，所以c 2 适合描述图形用户界面软件的体系结构的分析。但 是它也存在一定的不足，c 2 所提供的体系结构规约的语法标记符号没有相关语义的约 束，所以它不支持体系结构风格的规约和分析，只能应用于特定领域的研究工作。 u n i c o n 是s h a w 等开发的一种体系结构描述语言【2 5 1 。u n i c o n 运用连接件来规定组件 之间的交互机制。连接件是单独存在的、对称和非对称的，它运用系列角色( r o l e ) 定 义交互的参与者，而组件接口是系列扮演者( p l a y e r ) 。角色和扮演者用来表明组件希望 参与交互的性质和相关的交互细节，都具有类型和属性。u n i c o n 也存在着一定的不足， 一7 一 东北大学硕士学位论文第2 章研究基础 比如，它仅仅支持固定的交互类型和连接件，没有提供描述一类系统的机制和方法。其 次，u n i c o n 规约的组件和连接件同实现相关，体系结构模型与实现相互对应，是实现规 约语言，因此，u n i c o n 不能很好的描述体系结构风格规约。 r a p i d e 是l u c h h a m 等开发的一种体系结构描述语言【9 】。它基于偏序事件集p o s e r s ( p a r t i a l l yo r d e r e de v e n ts e t s ) 对组件的计算行为和交互行为进行系统分析和建模。它 与上述集中方法不同，是独立于实现的。r a p i d e 运用通信事件序列描述组件的行为，其 中通信事件又分为外部动作( e x t e m a c t i o n ) 和公共动作( p u b l i c a c t i o n ) 两类，通过观 察外部动作，再用连接件机制在组件接口的外部动作和公共动作之间建立关联，规定组 件之间事件发生的因果关系，从而描述组件和系统的行为。尽管如此，r a p i d e 还是存在 不足的地方，首先，因为r a p i d e 是应用连接件机制连接组件，类似于d a r w i n 的绑定， 所以它只能描述组件之间的非对称交互关系。其次，它的连接机制是嵌入配置定义中的， 不能单独对连接件进行描述和分析，还要分析连接件所嵌入的配置。 w r i g h t 是r o b e r t a l l e n 等开发的一种体系结构描述语割1 6 】。它以通信顺序进程c s p ( c o m m u n i c a t i o ns e q u e n c ep r o c e s s ) 为形式语义基础，侧重在高于实现层的抽象层次上 对体系结构的组件、连接件、配置三个方面进行描述。w r i g h t 运用c s p 描述组件端口 的交互行为和计算行为，并描述连接件的交互协议和角色规约。它先定义组件和连接件 的实例，并在相应的端口和角色之间建立连接( a t t a c h m e n t ) ，再给出系统的配置 ( c o n f i g u r a t i o n ) ，也可以通过绑定机制支持系统的层次架构。 与上述体系结构描述语言不同的是，w r i g h t 不仅能提供单个系统体系结构的分析和 规约，而且支持体系结构风格的分析和规约。它通过组件和连接件类型来定义体系结构 风格术语，用组件和连接件的相关约束机制来表示体系结构风格的属性。w r i g h t 还给出 了大量的体系结构静态分析机制，但它也存在着不足，比如c s p 固有的静态属性使得它 描述动态体系结构方面的能力有所欠缺，其次，它也没有考虑