（控制理论与控制工程专业论文）基于形式规格说明的统一软件建模系统的研究.pdf

上海大学工学博士学位论文 摘要 近年来，随着软件规模的不断扩大，复杂性不断增加，如何提高软件开发效 率，保证软件质量成为软件业界的中心问题。面向对象软件建模技术为提高大规 模软件开发的效率与质量带来了希望，为软件开发自动化奠定了基础。 面向对象软件建模语言u m l 以其图形化的表达及对软件设计提供各种各样 的支持而迅速成为软件业界的标准。它为设计人员提供了各种各样的视图、半形 式化的元模型语义、对设计元素的形式化逻辑约束。u m l 采用直观的图形表示 法，给使用者带来了方便，但同时图形表示法有模糊性，特别是需求分析模型中 语义描述用的是自然语言，使设计人员难以建立严格的需求模型，无法通过工具 自动完成模型内部的一致性检查、证明、验证；无法从需求模型自动或半自动地 获得设计模型，并保持模型间的一致。 形式化的软件规格说明建立在严格数学基础上，具有精确的符号表示，采用 严格的数学工具、具有精确数学语义，能够进行推理和演算，并适合工具处理。 因此，用形式方法来构建系统，可提高传统的结构性和易维护性，提高软件的质 量。 本文从提高u m l 模型的精度和模型一致性入手，将形式化的软件规格说明技术 应用到u m l 需求模型与设计模型的构建中，对面向对象的软件模型的框架、类模 型、交互模型、构件模型、体系结构模型，以及模型的静态特性与动态特性进行 了深入的研究。所做的工作和取得的成果主要体现在以下几个方面： 提出了一种基于形式规格说明和面向对象技术的软件建模策略。采用面 向对象建模方法，将统一建模语言u m l ( u n i f i e dm o d e l i n gl a n g u a g e ) 、 统一开发过程r u p ( r a t i o n a lu n i f i e dp r o c e s s ) 与统一程序设计理论u t p ( u n i f i e dt h e o r yo fp r o g r a m m i n g ) 相结合。分析了软件开发过程，并对 统一开发过程r u p 中涉及的模型进行了深入的研究，定义了概念类模型、 设计类模型、交互模型、构件模型、体系结构模型，并从语义上给出了 模型的良定义条件。 系统地提出了一系列提高u m l 软件模型精确性的策略。利用面向对象的 形式化规格说明语言o o l 建立了软件开发中涉及的各种动、静态模型， 给出了模型精确的形式化语义，从而可以从语义上分析所建模型的正确 性，以及设计模型相对于需求模型的正确性。 提出了保持静态模型与动态模型一致的策略。分析了r u p 中类模型与交 互模型的关系，根据模型的语义，给出了动静态模型一致的条件和实现 的策略。 提出了保持需求模型和设计模型一致以及下一迭代段与上一迭代段一致 的策略，既保持模型的横向一致又保持模型的纵向一致，并显示了如何 用模型精化的方法消除不一致。 v 上海大学工学博士学位论文 提出了一种基于设计模式( d e s i g np a t t e r n ) 的模型精化方法，通过委托 ( d e l i g a t i o n ) 、分解( d e c o m p o s i t i o n ) 和组合( c o m p o s i t i o n ) 将设计模型 进一步细化，以提高软件设计的自动化程度。 提出了一种通用的软件构建框架，并定义了构件模型、连接器模型和软 件体系结构模型。 该项研究主要有三个目的：一是将形式规格说明用于面向对象系统的建模， 并用r u p 中的迭代式方法进行推导，以适应大规模软件开发的需要，二是统一 r u p 中u m l 模型的各种不同视图，三是用形式方法提高u m l 和r u p 模型的准 确性，保证软件系统的质量。 我们总的目标是建立统一的软件开发模型系统，用形式规格说明技术增强 u m l 和r u p 的建模能力，提高模型的精确性和一致性，将u m l 的图形表示法 与形式规格说明技术相结合提高模型的可理解性、可跟踪性，使大型软件开发人 员能够准确地描述各种模型，并通过形式规格说明来保证需求模型、设计模型与 程序实现之间的一致；建立通用的软件构建框架，定义构件与体系结构模型；采 用迭代式软件开发，使系统在整个软件生命周期中，当需求发生变化时，设计人 员能够根据需求模型的变化局部性地修改设计模型，提高大型软件的安全性与开 发效率。 关键词：统一软件开发过程，统一建模语言，形式规格说明，统一程序设计理论。 v i 上海大学工学博士学位论文 a b s t r a c t i nr e c e n ty e a r s ，s o f t w a r ed e v e l o p m e n ts c a l eh a sl a r g e l yi n c r e a s e da n ds o f t w a r e b e c o m e sm o r ea n dm o r ec o m p l i c a t e d h o wt oi m p r o v et h ee f f i c i e n c yo fs 0 1 a r e d e v e l o p m e n ta n dk e e ps o f t w a r ea th i g hq u a l i t yh a v eb e c o m ek e yp r o b l e m si ns o f t w a r e i n d u s t r y o b j e c to r i e n t e dt e c h n o l o g yi st h em o s tp r o m i s i n go n et os o l v et h e s ep r o b l e m s o b j e c t o r i e n t e dt e c h n o l o g yi sa l s of u n d a m e n t a lt ot h ea u t o m a t i o no fs o f t w a r e d e v e l o p m e n t t 1 1 eu n i f i e dm o d e l i n gl a n g u a g eu m lp r o v i d e su s e r sw i t hg r a p h i cd e s c r i p t i o n e n v i r o n m e n t ，a l o n gw i t hv a r i o u sk i n d so f t o o l st os u p p o r ts o f t w a r ed e v e l o p m e n t ，a n d r a p i d l yb e c o m e sas t a n d a r do b j e c to r i e n t e ds o f t w a r em o d e l i n gl a n g u a g ei ns o f t w a r e i n d u s t r y u m lc o n t a i n sd i f f e r e n tk i n d so fv i e w s ，s e m i f o r m a ls e m a n t i c so f m a t am o d e l a n df o r m a lc o n s t r a i n t st ot h ee l e m e n t so fd e s i g n n l eg r a p h i cn o t a t i o no fu m li sv e r y c o n v e n i e n tf o ru s e r st ou n d e r s t a n da n du s e h o w e v e ri ti sn o tv e r yp r e c i s e e s p e c i a l l y f o rt h er e q u i r e m e n ta n a l y s i sm o d e l ，t h ed e s c r i p t i o nl a n g l l a g eu s e di nt h em o d e li s n a t u r a ll a n g u a g et h a tc a n n o tb eu s e dt om o d e lr e q u i r e m e n t sr i g o r o u s l y s ot h ed e s i g n e r c a n n o tc o n s t r u c tas t r i c tr e q u i r e m e n tm e d e la n dc h e c k ，o rp r o o fa n dv a l i d a t e ，t h e i n t e m a lc o n s i s t e n c ya u t o m a t i c a l l yw i t ht o o l s m o r e o v e r , t h e yc a n n o to b t a i nd e s i g n m o d e lf r o m r e q u i r e m e n tm o d e la u t o m a t i c a l l y o r s e m i - a u t o m a t i c a l l y a n dk e e p c o n s i s t e n c ya m o n gm o d e l s t h ef o r m a ls p e c i f i c a t i o ni ss t r i c t l yb a s e do nm a t h e m a t i c s ，w i t hp r e c i s es y m b o l i c n o t a t i o na n dm a t h e m a t i ct o o ls u p p o r t t h en o t a t i o nh a sr i g o r o u ss e m a n t i c sa n di se a s y t om a s o na n dc a l c u l a t e ，t h e r e b yi ss u i t a b l ef o rt o o lh a n d l e s ot h es y s t e m sc o n s t r u c t e d w i t hf o r m a lm e t h o d sa r eb e t t e ro r g a n i z e da n de a s i e rt om a i n t a i n ，t h u sa th i g h e rq u a l i t y t oi m p r o v et h ep r e c i s i o no fm o d e l sa n dk e e pc o n s i s t e n c ya m o n gt h e m ，w e c o n s t r u c tu m l r e q u i r e m e n tm o d e la n dd e s i g nm e d e lb a s e do nf o r m a lm e t h o d s w e t h o r o u g h l ys t u d yt h ef r a m e w o r ko fo os o f t w a r ec o n s t r u c t i o na n dt h es t a t i c d y n a m i c p r o p e r t i e so fm e d e l s ，i n c l u d i n gc l a s sm e d e l ，i n t e r a c t i o nm o d e l ，c o m p o n e n tm o d e la n d a r c h i t e c t u r em o d e i 0 1 1 1 r e s e a r c ho b j e c t i v e sa n dc o n t r i b u t i o nd i s c u s s e di nt h e d i s s e r t a t i o na r el i s t e da sf o l l o w s ： a no b j e c to r i e n t e ds o f t w a r em o d e l i n gs t r a t e g yi sp r o p o s e db a s e do nf o r m a l s p e c i f i c a t i o n u m l ( u n i f i e dm o d e l i n gl a n g u a g e ) 。r u p ( r a t i o n a lu n i f i e d p r o c e s s ) a n du t p ( u n i f i e dt h e o r yo f p r o g r a m m i n g ) a r ei n t e g r a t e d t h e p r o c e s so fs o f t w a r ed e v e l o p m e n ta n das e r i e so fm e d e l su s e di nr u pa r e s t u d i e dc a r e f u l l y , a n dam o d e ls y s t e mb a s e do nu m li sc o n s t r u c t e d w e d e f i n ec o n c e p t u a lm o d e l ，d e s i g nm o d e l ，i n t e r a c t i o nm o d e l ，c o m p o n e n tm o d e l a n da r c h i t e c t u r em o d e l ，a n dg i v et h ew e l l - d e f i n e d n e s sc o n d i t i o n s o ft h e m o d e l sa c c o r d i n gt os e m a n t i c sr e l a t e d 上海大学工学博士学位论文 w ep r o p o s eas e to f s t r a t e g i e s t o i m p r o v et h ep r e c i s i o no fm o d e l s t a t i c d 3 7 n a m i c m o d e l sa r ec o n s t r u c t e db a s e do no b j e c to r i e n t e df o r m a l s p e c i f i c a t i o nl a n g u a g eo o l i nt e r m so ft h ep r e c i s ef o r m a ls e m a n t i c so f m o d e l ，t h em e c h a n i s mo fc h e c k i n gt h ec o r r e c t n e s so fm o d e l sa n dd e s i g n m o d e lwr t u s e rr e q u i r e m e n t si sp r o p o s e d a s t r a t e g yt ok e e pc o n s i s t e n c yb e t w e e ns t a t i cm o d e la n dd y n a m i cm o d e li s p r o p o s e d a f t e ra n a l y z i n g t h er e l a t i o n s h i pb e t w e e nc l a s sm o d e la n d i n t e r a c t i o nm o d e lo fr u p , w eg i v et h ec o n s i s t e n c yc o n d i t i o n so fs t a t i cm o d e l a n dd y n a m i cm o d e la c c o r d i n gt ot h es e m a n t i c so fm o d e l s am e t h o di sp r o p o s e dt ok e 印c o n s i s t e n c yb e t w e e nr e q u i r e m e n tm o d e la n d d e s i g nm o d e la n dt h ec o n s i s t e n c yb e t w e e nd i f f e r e n ti t e r a t i o n s ，o rt h e h o r i z o n t a la n dv e r t i c a lc o n s i s t e n c y w ea l s os h o wh o wt oe l i m i n a t et h e i n c o n s i s t e n c yb ym o d e lr e f i n e m e n t am e t h o do f d e s i g nm o d e lr e f i n e m e n tb a s e do nm o d e lr e f i n e m e n ti sp r o p o s e d d e s i g nm o d e li sr e f m e db yd e l e g a t i o n ，d e c o m p o s i t i o na n dc o m p o s i t i o ni n o r d e rt oa p p r o a c ha u t o m a t i cp r o g r a m m i n g a g e n e r i cs o f t w a r ec o n s t r u c t i o nf r a m e w o r ki sp r o p o s e d a n da r c h i t e c t u r e m o d e la sw e l la sa na b s t r a c tc o m p o n e n tm o d e la n dc o n n e c t o rm o d e li s d e f i n e d t h e r ea r et h r e eo b j e c t i v e si no u i r e s e a r c h ：f i r s ti st oi n t e g r a t ef o r m a lm e t h o dw i t l l o b j e c to r i e n t e ds o f t w a r em o d e l i n gt e c h n o l o g y ；s e c o n di st ou _ n i f yv a r i o u sv i e w so f u m lm o d e l su s e di nr u p ；a n dt h i r di st oi m p r o v et h ea c c u r a c yo ft h em o d e lo fu m l a n dr u pt og u a r a n t e et h eq u a l i t yo fs o f t w a r es y s t e m 0 u ro v e r a l la i mi st oc o n s t r u c tau n i f i e ds o f t w a r ed e v e l o p m e n tm o d e ls y s t e m a n d e n h a n c et h em o d e l i n gc a p a b i l i t yo fu m la n dr u pw i t hf o r m a ls p e c i f i c a t i o n i n t e g r a t i n gf o r m a ls p e c i f i c a t i o nw i t ht h eg r a p h i cn o t a t i o no fu m lt od e s c r i b et h e m o d e lp r e c i s e l ya n di m p r o v et h eu n d e r s t a n d a b i l i t ya n dt r a c e a b i l i t yo ft h em o d e l ，s o t h a tt h ed e v e l o p e r so fl a r g e - s c a l es o f t w a r ed e v e l o p m e n tc a nd e s c r i b e t h em o d e l s p r e c i s e l ya n dk e e pc o n s i s t e n c ya m o n gr e q u i r e m e n tm o d e l ，d e s i g nm o d e la n dt h e i m p l e m e n t a t i o n w jc o n s t r u c tag e n e r i cs o f t w a r ec o n s t r u c t i o nf r a m e w o r ka n dd e f i n e t h ec o m p o n e n tm o d e la sw e l la st h ea r c h i t e c t u r em o d e l t h ei 把r a t i v ed e v e l o p m e n t p r o c e s se n a b l e st h ed e v e l o p e r st om o d i f yt h em o d e l sp a r t l ya c c o r d i n gt ot h eu p d a t e d r e q u i r e m e n t sw h e nt h eu s e rr e q u i r e m e n t sa r ec h a n g e di nt h ew h o l es o r w a r el i f cc y c l e ， t h u si m p r o v et h er e l i a b i l i t yo f t h es y s t e ma n dt h ee 伍c i e n c yo f s o f t w a r ed e v e l o p m e n t k e y w o r d s ：u n i f i e dp r o c e s s ，u n i f i e dm o d e l i n gl a n g u a g e ，f o r m a ls p e c i f i c a t i o n ，u n i f i e d t h e o r yo f p r o g r a m m i n g v 1 1 1 上海大学工学博士学位论文 原创性声明 本人声明：所呈交的论文是本人在导师指导下进行的研究工作。 除了文中特别加以标注和致谢的地方外，论文中不包含其他人已发表 或撰写过的研究成果。参与同一工作的其他同志对本研究所做的任何 贡献均已在论文中作了明确的说明并表示了谢意。 本论文使用授权说明 期壁兰! ! 本人完全了解上海大学有关保留、使用学位论文的规定，即：学校有权保留论文及送交 论文复印件，允许论文被查阅和借阅；学校可以公布论文的全部或部分内容。 ( 保密的论文在解密后应遵守此规定) i i 上海大学工学博士学位论文 第一章引言 现代软件系统必须既可靠又高效。实际上，软件开发过程就是对实际问题进 行建模，并转换、精化模型，直至生成可执行代码的过程【l 】。软件工程一直面临 的巨大挑战是如何建立从需求分析到设计直到实现的各种层次的软件模型；如何 通过模型的精化从上一层模型获得下一层模型。设计人员一般按照功能性、非功 能性的需求建立需求模型，再由需求模型获得满足需求的设计。在实践中，由于 软件开发中涉及的模型层次是多种的，建模的视角是多样的，因此软件建模工作 非常复杂。在软件开发中我们首先要问： 如何建立软件系统各层次模型? 各层次模型之间有什么关系? 什么是需求模型? 如何精确地表达需求模型? 如何保证设计模型是根据需求模型构造的? 1 1 简介 通常构造程序是困难的，但跟踪程序的更改和更改带来连锁反应则更加困难。 因为构造程序涉及分析、设计、实现各个阶段，要跟踪所有模型和模型的更改， 并保证软件生命周期中不同时期的模型一致没有合适的方法，是无法完成的。 要保持各种模型精确、一致不仅非常困难、代价高昂而且容易出错。为了提高软 件的可靠性，并方便软件分析、设计和演化，很多设计人员使用一些比较有效的 工具或方法。例如，统一建模语言( u n i f i e dm o d e l i n gl a n g u a g e ，简写为u m l ) 为软件开发过程中建立软件模型带来了方便，它提高了模型的可维护性与可重 用性。另一种被广泛接受的方法是设计模式。同样，框架及基于构件的软件工程 ( c o m p o n e n tb a s e ds o f t w a r ee n g i n e e r i n g ，简写为c b s e ) 为用户进行构件的熏用 与组合提供了商效的工具。但和其他非形式化或半形式化方法一样，上述方法缺 少形式化语义的支持。它们不是良构的( w e l l f o u n d e d ) ：不能精确地描述需求； 不能将需求模型与设计模型连为一体，使设计人员可以验证设计模型严格地表达 需求模型；不能直接从需求获得设计。 另外，u m l 作为一种事实上的标准建模语言，提供了多种类型的视图供设计 人员或用户从不同的抽象层次和不同视角描述模型。但有时同一系统的不同视图 之间可能是不一致的。不一致问题分为横向不一致与纵向不一致，横向不一致指 同一抽象层次，不同视角模型之间的不一致，纵向不一致指不同抽象层次模型之 间的不一致 3 】。 r a t i o n a l 公司为了增强u m l 的表达能力，一直力图提供形式化建模的工具， 使图形化建模方法与形式化表示法结合起来，提高模型的精确性。u m l 确实提 供了一些形式化扩充，包括对象约束语言o c l ( o b j e e t c o n s t r a i n l a n g u a g e ) 。o c l 是一阶谓词逻辑与图形导航语言( d i a g r a m n a v i g a t i o n l a n g u a g e ) 相结合的产物m 1 。 虽然o c l 作为标准的u m l 的一部分，可以直接和u m l 关联起来，但目前o c l 的表达能力还不够强，虽然可以用u m l 中的对象约束语言o c l 来表示语法一致 的条件，但无法用它来表达模型的动态语义。o c l 的语义是建立在u m l 语义之 上海大学工学博士学位论文 上的，而两者的集成仅仅通过自然语言来实现，o c l 本身没有元模型，结果就导 致o c l 的语义和表示法之间没有明显的区分。这使精确地解释o c l 出现了问题。 例如u m l 模型中o c l 表达式没有完整地定义语境。没有o c l 元模型。要通过 x m i 来结构化地交换o c l 约束就不可能了( 尽管可将其视为未经解释的字符串) ， 而且也很难保证在软件实现过程中o c l 描述之间的一致性。0 c l 目前还无法表 达软件开发过程中所涉及到的所有模型，且没有工具支持各种模型的分析、处理 和模型的演变。 统一软件开发过程r u p 是近年随着软件规模的增大、复杂性的提高以及对软 件便于演化的要求而发展起来的。r u p 可以使用u m l 中的各种工具。在基于u m l 的开发过程( 如r u p 6 】) 中，用于表达和分析系统开发某个特定阶段创建的模 型的主要有几种类型的u m l 视图：类图( c l a s sd i a g r a m ) 表示静态结构( 静态视 图s t a t i cv i e w ) ：状态图表示动态行为规格说明和验证( 行为视图b e h a v i o r a lv i e w ) ， 顺序图和协作图表示对象之间的交互( 交互视图i n t e r a c t i o nv i e w ) ；o c l 表示对 象的功能和约束( 功能视图f u n c t i o n a lv i e w ) 等。u m l 多视角建模有其优点。每 一视角关注某方面的问题，使设计人员可以分析和理解系统不同方面的特性f t 。 但多视角建模主要需要解决以下几方面的问题： 模型一致( m o d e lc o n s i s t e n c y ) ：即系统各视角的模型都必须与其子模型 在语法上和语义上一致。而语义一致首先要满足语法致。 模型转换和演化( m o d e lt r a n s f o r m a t i o na n de v o l u t i o n ) ：即要精化化后的 模型与精化前的模型语义一致纵向一致f 。 模型跟踪( m o d e lt r a c e a b i l i t y ) ：即模型一个视图更改引起其它子模型中 一致的更改。 模型集成( m o l li n t e g r a t i o n ) ：即需要将个视图组合起来才能产生系统。 解决以上问题是模型驱动开发( m o l ld r i v e nd e v e l o p m e n t ) 的核心i l j 。近年 来，人们在形式化u m l 构建软件开发框架方面已经做了一些研究工作 3 , 6 , 9 1 。【1 0 】 定义了一种规格说明表示法并开发了一种面向对象程序设计的糖化演算。在【1 1 1 2 1 中我们分析了如何建立需求分析的u m l 模型，如何将模型形式化。我们在【”】中 分析了大型软件开发的过程，并设计了一种适于重用的开发框架。在【1 4 1 中我们研 究了如何使u m l 设计模型与需求模型相容。我们还在上述工作的基础上，提出 一种基于规格说明的统一软件开发过程模型的建模方法。针对当前软件开发的特 点，我们采用面向对象建模策略，将统一建模语言u m l ( u n i f l e dm o d e l i n g l a n g u a g e ) 、统一开发过程r u p ( r a t i o n a lu n i f i e dp r o c e s s ) 与统一程序设计理论 u t p ( u n i f i e dt h e o r yo fp r o g r a m m i n g ) 相结合来建模。用形式方法来增强u m l 和r u p 的建模能力，使大型软件开发人员在利用u m l 提供的图形表示法建立模 型时，可以用形式方法对模型进行严格的描述，提高模型的精确性、可理解性、 可跟踪性。 u m l 模型的一致性方面的研究目前比较热。文章例研究了系统不同状态图之 间特定类型行为的一致性问题，它将状态图转换成c s p i l 5 】。文掣1 6 】研究了系统设 计类图和顺序图之间横向语法一致性问题。文章【l l1 8 , 1 9 , 2 0 , ”】都是针对一致性方 面问题的。但那些工作主要集中在单个图的形式化和一、二种模型的一致性方面， 如类图和状态图的一致性。据检索，目前很少有系统地处理u m l 模型精化方面 的工作。另外研究中的另一种现象是不同的研究团体侧重不同的模型( 如顺序图 上海大学工学博士学位论文 和状态机) 。导致失去多视角建模的缀多优点，增加了菜些类型模型的复杂性， 降低了u m l 模型的作用。 很多研究人员已经意识到解决一致性问题的艰难1 7 8 1 。一致性的条件和解决方 案与所涉及的图、开发过程、开发阶段有关。事实上，造成不一致的根源就是 u m l 的图形表示法。由于u m l 图形没有精确的语义，定义和检查模型一致性就 很困难。相对于形式化模型来说，图形式模型的( 非形式化) 语义和语法的限制 较少，随意的特性太多：类图中的角色名和颞序图中的对象名都是随意的。 我们基于u m l 和【9 ，玎j 中的形式化规格说明表示法，提出了一种表示u m l 类 模型和交互图的方法。然后，提供形式化的u m l 需求模型和设计模型。并按照 精化来定义设计模型与需求模型的形式化连接( f o r m a ll i n k ) 2 ，按糟化演算【1 0 1 对关系迸行推理。 主要步骤是先建立需求分析和软件设计的u m l 形式化模型，采用迭代式软 件开发模型，将开发过程分成一系列小的迭代段，每个迭代段仅处理一个小的模 型，系统随着迭代的继续逐步增大。迭代式软件开发可以使系统在整个软件生命 周期中，当需求发生变化时，设计人员能够根据需求模型的变化局部性地修改设 计模型，提高大型软件的安全性与开发效率。 我们使用 2 4 】中定义的面向对象的形式化规格说明语言( o b j e c t o r i e n t e d s p e c i f i c a t i o nl a n g u a g e ，简称o o l ) 给出集成的u m l 系统形式化模型并研究如何使 面向对象设计的精化演算( r e f m e m e n tc a l c u l u sf o ro b j e c t - o r i e n t e dd e s i g n s ，简称 r c o o d ) 支持分析与开发系统模型。精化保证了系统某一个模型发生更改对， 其它模型相应改变，系统各模型保持一致，并保证系统的正确性。 我们还提出了一种层次化的通用软件构建框架，并定义了构件模型与软件体 系结构模型，构件模型是建立在类模型层次之上的，而体系结构模型又是由构件 和构件连接递归定义的。通过模型形式化和可执行的u m l ( e x e c u t a b l eu m l ) ，我 们的方法有望用于支持模型驱动开发( m o d e ld r i v e n d e v e l o p m e n t ，简称m d v ) 【1 1 l 。 1 2 策略概要 我们主要研究r u p 增量式开发的特点和基于构件的面向对象软件开发方法， 探讨下列闯题； 如何建立迭代式开发中形式化的u m l 需求模型，并保证模型的静态视图 与动态视图一致? 如何建立某一个迭代段中形式化的u m l 设计模型，并保证模型的静态视 图和动态交互视图一致? 如何使某一迭代段内的设计模型与需求模型严格相关? 如何傈证后续迭代段中模型的一致性与正确性? 如何利用设计模式对设计模型进行精化? 如何建立利于重用与构件组合的系统构建框架，及相应的构件与体系结 构模型? m d v 已经成为u m l 大会的热点，2 0 0 3 年u m l 大会上有一个该专题的研讨会( w o r k s h o p ) 和一个座谈 会f p a n e l ) 。 上海大学工学博士学位论文 u m l 虽然被广泛应用于多个领域并已成为面向对象软件建模的标准，可从多 视角建模。但由于缺少完整的形式方法支持，所以既无法严格推理验证各阶段设 计的正确性，保证各个设计模型良定义，又无法对不同阶段模型之间的一致性进 行形式化的检查。所以在设计安全性非常重要的应用程序时，就需要将形式方法 和u m l 结合起来。 我们首先分析了面向对象的设计演算系统，该系统包括面向对象的形式化规 格说明语言( o o l ) 和精化演算。精化演算基于h o a r e 和j i f e n gh e 的统一程序 设计理论( u n i f i e dt h e o r i e so fp r o g r a m m i n g ，简称u t p ) 阻”。然后研究如何用设 计演算形式化地表达u m l 需求与设计模型，进行模型推理。 我们提出一种开发策略，用一个四元组m = ，f ，q ， 来表示系统模型。 其中是类图2 ，f 是一系列顺序图，q 是一系列状态机，0 是系统约束。类图中 的有些类和关联是概念性的，有些是设计类图和关联。概念类中没有方法，且属 性都是公有的。可以往概念类图中添加一些方法以实现某些任务 2 6 1 ，或将某些属 性改成私有或保护的以利封装，使概念类图精化成设计类图。概念类图中的关联 是无方向的。当任务分配方向确定后，概念关联就精化成设计关联。软件开发过 程是从建立需求模型开始的，需求模型可表示为r m = ，类图 r 中所包含的所有类和关联都是概念性的。图1 1 是一个概念类图的示例，表示 一个零售店的自动结帐系统弘“。 图1 - 1 商店自动结帐系统 顺序图r r 描述用例中执行者和系统之间的交互，状态机g 描述用例的行为和 功能。此类模型可以通过横向精化( h o r i z o n t a lr e f i n e m e n t ) 构建，逐步加入更多 的信息和用例。一个开发周期要经过一系列的精化，才能将需求模型转化成设计 模型： d m l = r m i e m l e ，m n 量d m 在设计类图d 1 中，只有设计类和关联。在下一迭代段( i t e r a t i o n ) 中，我们 通过用例、概念类图、关联来添加用户需求。此迭代式开发过程如图1 - 2 所示。 2 为简单起见，我们不考虑u m l 包。 4 上海大学t - 学博士学位论文 早妄，圃i n i 九 i n 。 n 匈二回呈回 图1 - 2r u p 统一软件开发过程 将精化演算与r u p 结合起来，使得迭代式开发中设计演算的使用效率更高， 使得每一步迭代只需要处理一个较小的模型。 将形式方法与r u p 结合起来可以增强r u p 的描述能力，建立更加严格、一 致、准确的软件模型，并可以将需求分析、软件体系结构、设计、实现集成起来， 建立统一的开发模型。本文基于统一程序设计理论，将形式方法与r u p 结合起 来，建立迭代式软件开发模型，以适应大型软件开发的环境，并可通过推理、验 证保证同一迭代段的需求模型与设计模型之间、上迭代段与下一迭代段的需求 模型之间、设计模型之间的一致性。 笛m 上海大学工学博士学位论文 第二章统一建模语言 对象建模是软件工程的一个研究领域，和软件产业中的实践密切相关。软件 需求、限制、目标都来自用户。来自用户的要求通常既复杂，数量又多；对象建 模需要有一些技术帮助我们将要放入软件的东西形式化。由于软件需要用编程语 言逐步写代码，因此还需要另一些技术来表达软件是如何构建的，特别是软件的 内部组织。 事实上，对象建模的基础是抽象，如在某个时刻，审慎地忽略系统的某些特 性，突出另外一些特性。它的成功之处在于添加新的特征或新操作时，结构不需 要改变。特别是在需求工程中，能临时添加细节是很重要的。对象模型需要很好 地捕捉并表达用户的需要，并能进行精化。 对象建模的另一个基础是对象范例本身。我们对系统的考虑是层次化的，每 一个新的、更详细的模型都是从前一步模型映射来的。用对象、类、类型、关系 和交互来创建模型被认为是一种较好的方式，该方式可提高需求跟踪性和软件质 量。面向对象建模使我们可以分离并获取软件的安全部分，以提高重用性、可维 护性和可靠性。 从工业界看来，目前有多种商业发展趋势，这些趋势正使得软件开发小组之 间的沟通更加困难。首先是小型公司并入大型公司。这种合并常常带来更大的整 体业务效率，这些公司的i t 部门很可能面临困难的开发过程以及不同的沟通机 制。一个小组可能接管另一个小组的职责，他们就需要开发工具帮助其理解并维 护现有的软件项目。另外一个趋势就是海p b i t s b 包的增加。在这个方面，有地理 上分隔的问题，也有语言与文化障碍的问题。随着这些趋势的继续向前演变，任 何有助于解决沟通困难的工具将为公司( 或机构) 带来巨大的竞争优势。一个可 视化图超越了语言与文化障碍，能让分散的开发小组方便地开展工作。统一建模 语言u m l 能跨越沟通隔阂，使开发小组之间的合作更加高效。 从1 9 8 9 年到1 9 9 4 年，建模语言的数量从不n l o e e 增加到y s o 多种，一度爆发 了“方法大战”。2 0 世纪9 0 年代中期，出现了一批新方法，最引人注目的是b o o t h 1 9 9 3 、0 0 s e 和o m t - 2 等。各种建模语言，尽管各有千秋，但存在一些差别，这 极大地妨碍了用户问的交流。人们普遍认为，软件工程领域在最近几年内取得了 前所未有的进展，其成果超过软件工程领域过去十至十五年来的成就总和。其中 最重要的成果之一就是标准建模语言u m l 的出现。标准建模语言u m l 为可视化 建模软件的开发奠定了坚实的基础。u m l 不仅支持面向对象的分析与设计，还支 持从需求分析开始的软件开发全过程。但是，如果由开发人员手工地绘制这些图 形，不仅非常烦琐，而且很难保证不同图形之间的一致性，也无法通过模拟来预 测系统的行为。如果客观需求发生变化，就要重画这些图形，这不仅有大量的工 作需要重复进行。影响效率，而且对开发人员的心理有极为不利的负面影响。因 此研究与开发标准建模语言u m l 的支持环境势在必行。如何恰当地将可视化图形 建模技术用于解决软件开发所面临的问题以及对建模过程和支持工具的研究。是 目前国际上的热点课题。我们也正在积极开展u m l 集成化支持环境等方面的研究 上海大学工学博士学住论文 与开发工作，并取得了一定的成果。本章首先介绍u m l 的主要内容，分析存在的 问题，探讨可能的解决方案。并讨论迭代式软件开发过程r u p 的实现。 2 1 统一建模语言u m l 统一建模语言( u m l ) 是3