（计算机软件与理论专业论文）uml建模的形式化研究.pdf

兰州大学硕士学位论文 u m l 建模的形式化研究 摘要 统一建模语言( u m l ) 己经成为软件建模事实上的标准，但是它也存在不少问 题。尽管u m l 大部分的语法已经定义，并给出了静态语义，但是动态语义大部分 只是用自然语言描述，经常产生模糊或歧义，或者干脆没有给出语义。因此，对 u m l 进行形式语义研究，对增进该语言的准确性、一致性和可扩展性是十分有帮 助的，为模型的正确性证明、转换以及支持u m l 建模工具的一致性检查提供了有 力的理论工具。 本文首先介绍了形式化方法和z 语言，然后引入了一种面向对象的形式化规 格说明语言o o z s ，借助于该语言对u m l 的类图、用例图、状态图和顺序图进行 形式化描述，给出了这四种图的所有模型元素的语法描述和操作语义，从而建立 了一种从图形加文字的非形式化模型到具有数学基础的形式化模型的映射，在此 基础之上，可以进一步地进行模型一致性检测、代码半自动生成、测试用例自动 产生、程序正确性验证等工作。 关键字：u m lo o z s 形式化语义 兰州大学硕士学位论文 u m l 建模的形式化研究 a b s t r a c t a sad ef a c t os t a n d a r do fo b j e c t e d o 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 e ，u m l h a ss u c c e e d e di na n a l y s i sa n dd e s i g n so fm a n ys y s t e m s h o w e v e r , i ta l s oh a sm a n y f l a w s a l t h o u g ht h em a i np a r to fu m ls y n m xh a sb e e nw e l ld e f i n e d ，a sw e l la st h e s t a t i cs e m a n t i c s ，t h ed y n a m i cs e m a n t i c si sa l m o s td e s c r i b e di nn a t u r a ll a n g u a g e a sa r e s u l t ，t h e r ei sf r e q u e n t l ya m b i g u i t ya n dv a g u e n e s si nu m ls p e c i f i c a t i o n s ，t h e r e f o r e ， t h ef o r m a ls e m a n t i c s t u d yo fu m li sv e r yh e l p f u lf o r t h ei m p r o v e m e n to ft h e c l a r i f i c a t i o n ，e q u i v a l e n c e ，c o n s i s t e n c y , a n de x t e n d i b i l i t yo ft h el a n g u a g e ，t h u so f f e r sa p o w e r f u lt h e o r e t i c a lt o o lf o r t h ev a l i d i t yp r o o f , t r a n s i t i o no ft h em o d e la n dt h e c o n s i s t e n c yc h e c k o f t h em o d e l i n gt o o l ss u p p o s i n gu m l t h ef o r e p a r to ft h i st h e s i si s m a i n l ya b o u tf o r m a lm e t h o d s ，o o z sa n du m l o o z si sa no b j e c t e d o r i e n t e df o r m a ls p e c i f i c a t i o nl a n g u a g ee v o l v e df r o mz l a n g u a g e i nt h ef o l l o w i n gp a r t , f o u ru m l d i a g r a m s ：c l a s sd i a g r a m ，u s ec a s ed i a g r a m ，s t a t e c h a r t d i a g r a ma n ds e q u e n c ed i a g r a ma r ef o r m a l i z e du s i n go o z s t h a t i s ，a l lm o d e l e l e m e n t so ft h e s ef o u rd i a g r a m sa r er e p r e s e n t e db yi t sf o r m a ls y n t a xa n ds e m a n t i c s a c c o r d i n gt ot h ea b o v ew o r k ，am a p p i n gf r o mn o n f o r m a lm o d e lw h i c hi sc o m p o s e d o fg r a p h sa n dl e t t e r st of o r m a lm o d e lb a s e do nm a t h e m a t i c si sa c t u a l l yb u i l t f u r t h e r w o r ki n c l u d e sm o d e l c o n s i s t e n c yc h e c k i n g ，c o d ea u t o g e n e r a t i o n ，t e s t c a s e a u t o g e n e r a t i o n ，p r o g r a mv a l i d i t yv e r i f i c a t i o ne t c k e y w o r d s ：u m l o o z sf o r m a l i z a t i o ns e m a n t i c s 兰州大学碗士学位论文 u m l 建模的形式他研究 原创性声明 本久郑重声鞠：本入席量交盼学蕴论文，是在导瘁翡指导下独立 进行研究所取得的成果。学位论文中凡弓| 用他人园经发表或未发 表的残暴、数豢、观点等，均毫鹱确注鹱爨楚。除文孛已经淀骥 引用的肉容外，不包含任何其他个人或集体舀经发表绒撰写过的科研 残暴。对本文的磷究成巢傲寤煎要贡献的个人衣集钵，均已在文中数 明确方式标明。 本声龋的法律责任由本人承担。 论文作者签名： 弗凳， 日期： 0 、y ，谚 兰卅i 大学硕士学位论文 u m l 建模的形式化研究 关于学位论文使用授权的声明 本人在导师指导下所完成的论文及相关的职务作品，知识产权归 属兰州大学。本人完全了解兰州大学有关保存、使用学位论文的规定， 同意学校保存或向国家有关部门或机构送交论文的纸质版和电子版， 允许论文被查阅和借阅；本人授权兰州大学可以将本学位论文的全部 或部分内容编入有关数据库进行检索，可以采用任何复制手段保存和 汇编本学位论文。本人离校后发表、使用学位论文或与该论文直接相 关的学术论文或成果时，第一署名单位仍然为兰州大学。 保密论文在解密后应遵守此规定。 论文作者签名： 蓝基导师签名 期矽善上、弱 兰州大学硕士学位论文 u m l 建模的形式化研究 1 1 背景介绍 第一章引言 随着各种软件过程方法、编程语言和辅助开发工具的出现，软件研发人员 所需要考虑的计算的层面越来越抽象，越来越集中于业务逻辑而非在计算平台 上的实现细节。因此，对软件建模的研究受到越来越多的重视。 2 0 世纪8 0 年代出现的面向对象技术是软件技术的一次革命，系统分析人 员开始借助于面向对象技术对将要建造的软件系统建模。这些模型元素几乎和 代码元素相同，所以从模型生成代码非常简单、有效。而且用模型代替代码进 行设计，使研发人员可以在更高的抽象层次上讨论问题，避免了对代码语法的 不必要纠缠。随着面向对象建模技术飞速的发展，出现了一大批面向对象的软 件建模方法，新的问题也随之而生。由于不同的研究者各自为政，缺乏协作， 以至于在建模领域出现了所谓的“方法战争”。方法的提出者及其支持者们与其 他方法的支持者互相攻击，坚持自己的方法是最好的；工具开发商不得不耗时 费力地在同一个工具里支持大量不同的图形、符号、表示法，而软件开发人员 面对众多的方法、工具则显得无所适从。这些现象表明，提供一个软件建模的 全面解决方案已经成为当务之急，它必须是灵活的、可扩展的、可靠的、实用 的，以满足目前软件开发的需求和将来的发展。 统一建模语言( u n i f i e dm o d e l i n gl a n g u a g e ，u m l ) 是面向对象分析与设计 ( o o a & d ) 浪潮的产物，它已经成为了o m g 标准。u m l 的优势主要体现在可 以使用单一的集成的表示法来对系统的多个方面进行建模，模型范畴包括从系 统的静态结构到动态行为特征、从系统的逻辑功能到物理部署。因此，u m l 得 到了学术界和企业界的广泛支持，经过多年的完善，u m l 己经成为软件建模事 实上的标准。 但是，u m l 也存在不少问题，尤其是它缺乏一个精确的形式化的语义，这 使得对个u m l 模型的理解可能会有歧义；另一方面，在u m l 描绘系统不同 方面的各种模型之间也容易存在不一致性，因此难以实现逐步求精的开发过程， 难以对模型进行分析以保证其正确性。于是，u m l 的形式化语义研究成为一个 兰州大学硕士学位论文 u m l 建模的形式化研究 新兴的领域，不少组织和个人提出了大批的解决方案。本文正是在前人的研 究基础上，使用一种具有面向对象特征的形式化规格说明语言，来对u m l 的 四种图形进行形式化描述，使得分析人员利用u m l 建立的系统模型满足形式 化规约的要求。 1 2 本文的主要工作及其意义 u m l 的体系结构定义在一个四层的概念框架中，这四层分别是：用户对象 层、模型层、元模型层和元元模型层。用户对象描述的是特定问题域的具体事 物；模型描述这些事物的抽象原型及其规则，其表现形式就是开发人员所画出 的各种u m l 图及其附加的注释、说明等；而u m l 元模型则规定了应如何去建 立这些模型，也就是u m l 的各类视图、图及其组成元素的形式和规则。 本文的研究范畴就处于元模型层，主要工作围绕着四种l r m l 图进行：作 为系统结构模型的核心的类图、描述系统与用户交互的用例图、描述系统动态 行为特征的状态图和描述系统内部对象之间通信的顺序图。本文使用o o z s 语 言来对这四种图进行形式化： 用o o z s 给出图中的所有元素的语法描述及其静态的语义约束 对整个图定义一系列的语义模式，来刻画图的语义 本文的工作实际上建立了一种从图形加文字的非形式化模型到具有数学基 础的形式化模型的映射，在此基础之上，可以进一步地进行代码半自动生成、 测试用例自动产生、模型一致性检测、程序正确性验证等工作。例如，将形式 化的顺序图集成到类图之后，可以很方便地生成类的代码和类的测试用例。 1 3 本文的结构 本文共分五章，第一章阐述了本文的研究背景、主要工作和组织结构；第 二章是形式化方法的概述，重点介绍了z 语言、z 规格说明的结构以及在此基 础之上发展而来的o o z s ；第三章介绍了u m l 的发展历史、主要内容及其优缺 点，重点介绍了u m l 的元模型；第四章依次给出了u m l 类图、用例图、状态 图和顺序图的形式化描述：第五章是对本文工作的总结和对未来工作的展望。 兰州大学硕士学位论史u m l 建模的形式化研究 第二章形式化方法 2 1 形式化方法介绍 2 1 1 形式化方法的主要研究内容 形式化方法( f o r m a lm e t h o d s ) 是一种用于规范、设汁和验证计算机系统的基 于数学的方法，包括各种语言、技术和工具等。形式化方法可分为形式规约 ( f o r m a ls p e c i f i c a t i o n ，也称形式规范或形式化描述) 方法和形式验证( f o r m a l v e r i f i c a t i o n ) 方法两大类，形式规约方法包括了各种基于数学的表示法、语言咀 及对应的工具，形式验证方法包括各种模型检查器、定理证明器以及证明和验 证的方法等【1 1 。 ( 1 ) 形式规约 形式规约是用具有精确语义的形式语言书写的程序功能描述，它是设计和 编写程序的出发点，也是验证程序是否正确的依据。对形式规约通常要讨论其 一致性和完备性。 不同的形式规约方法要求不同的形式规约语言，即用于书写形式规约的语 言( 也称形式化描述语言) ，如用于系统建模的语言z 、b 等；代数语言o b j 等； 进程代数语言c s p 、c c s 等；时序逻辑语言t l a 、c t l 等以及用于集成的形 式规约方法的语言s d l 和r a i s e 。这些规约语言由于基于不同的数学理论及规 约方法，因而也千差万别，但它们有一个共同的特点，即每种规约语言均由基 本成分和构造成分两部分构成。前者用来描述基本( 原子) 规约，后者把基本部 分组合成大规约。构造成分是形式规约研究和设计的重点，也是衡量规约语言 优劣的主要依据。 ( 2 ) 形式验证 形式验证是用严格的数学方法来推理验证某一产品或设计是否符合其全部 或部分规范的过程。形式验证要求产品的规范有严格的形式化描述。目前形式 验证的研究主要有两类：模型检验( m o d e lc h e c k i n g ) 和定理证明( t h e o r e m p r o v i n g ) ，都是使用形式化方法来分析一个系统是否满足所期望的特性。 兰州大学硕：匕学位论文 u m l 建模的形式化研究 2 1 2 形式化方法研究的意义 软件需求的描述是软件开发的基础，而一般非形式化的需求说明很可能导 致不明确和不一致，并由此导致系统殴计上的错误，形式化方法则要求描述的 明确性，而描述的不一致性也就相对易于发现。由于有了软件需求的形式化规 约，设计人员就可以检验软件的设计是否满足软件的要求。对于编程来讲，甚 至可以考虑代码的自动生成。对于一些简单的系统，有可能将形式化的描述直 接转换成可执行程序，这就简化了软件开发过程，减少了产生错误的可能性， 也节约了软件开发的时间和资源成本。另外，形式化方法可以用于系统的验证， 以保证其正确性。对于测试来讲，形式化方法可用于测试用例的自动生成，这 可以节约许多时间和在一定程度上保证测试用例的覆盖率。 形式化方法在软件开发中一般用于类型检查、有效性验证、致性检查、 行为预测以及设计求精验证。通常以目前的软件开发方法为出发点，研究怎样 将这些方法形式化，使软件系统的描述精确化，以减少可能的误解所带来的问 题；或以目前常用的软件开发过程为出发点，研究怎样在软件开发过程中增加 一些形式化方法的应用，以提高软件的可靠性。 2 1 3 形式化方法的发展方向 ( 1 ) 形式化方法存在的问题 2 】 尽管形式化方法在软件工程及其相关的计算机领域已取得了成功，但是与 面向对象技术和g u 技术相比，其实用性还存在很大的差距。现有的技术应用 更多的是局限于大学、科研机构和对安全性要求极高的工业部门。其主要的问 题在于： 由于形式化方法是以计算逻辑、代数理论和软件结构为基础，因而它在 本质上是一种严格的、灵活性较差的方法，缺乏必要的实施手段和支持工具， 所以难以在实际工业开发过程中被广泛的接受。 现有的形式化方法在解决小规模的问题时较为有效，但却无法或很难应 用于一些较大规模的开发过程中。 形式化方法和软件开发过程难以平滑的结合。 兰州大学硕士学位论文 u m l 建模的形式化研究 尚没有一种形式化方法能够对软件工程生命周期的各个阶段提供全面的 支持。其中，缺乏有效的实施手段无疑是限制形式化方法进一步发展的核心因 素。 ( 2 ) 形式化方法与面向对象技术的结合 目前，将面向对象技术与形式化技术结合起来已成为了当前软件工程研究 的一个较热的领域。概括来说，主要有如下两个研究分支： 使用面向对象的结构来提高形式记号法的形式表达能力。 使用形式方法来分析面向对象的语义或提高这些记号法的表达对象概 念的能力。 形式方法与面向对象方法的结合，能够充分发挥两种方法各自的优点，起 到取长补短的效果。特别是第一种途径用面向对象机制扩展形式规格说明 语言，已经取得了较广的应用范围，例如对z ，v d m 等的面向对象扩充。 2 2 z 规格说明方法 2 2 1z 语言简介 z 语言是上世纪7 0 年代末、8 0 年代初由牛津大学程序设计研究组( r p g ) 设计的种形式化规格说明语言，主要用来在软件开发过程中说明软件系统的 需求和功能，并考虑软件的验证和求精等问题，因而也被称为z 规格说明方法。 在8 0 年代末，人们已经定义出了z 语言的标准文本。从9 0 年代开始，美、英、 日等国都对z 进行了深入的研究和开发，人们还把z 和结构化的分析方法、面向 对象的方法和程序变换等课题结合起来研究。蓑于z 的研究成果交流的zu s e r m e e t i n g ( z u m ) 基本上每年一届，已成为一个重要的国际学术会议。在每年的 i e e e 有关软件工程的国际学术会议上，也有不少关于z 的研究成果的报道，国 内也有些学者对此进行研究，并取得了不少成果”j 。 z 语言基于一阶谓词逻辑和集合论，可以对软件系统进行精确、无歧义且 可证明的规约。z 语言的一个主要的特点是可以对z 规格说明进行推理和证明， 这使得软件开发人员能够很快找出规格说明中的不一致、不完整之处，以便尽 早地发现需求中的隐患，从而降低开发成本。这一点在大型系统的应用中尤其 兰州大学硕士学位论文 u m l 建模的形式化研究 明显。 2 2 2z 语言的基本构造单元 z 是一种面向模型的规约方法，它主要用一些抽象的数学模型来描述目标 系统某一部分的数据类型、结构特征和行为特征。 ( 1 ) 模式 z 语言中定义了一种特殊的图形方式：模式( s c h e m a ) ，作为规格说明的基 本结构。可以用各种合适的模式来描述系统的各个层次上的抽象状态和操作。 一个完整的软件系统可阻分解为若干层、若干个模式，这样就可以把复杂的系 统分成一个个便于控制的小模块。 按功能的不同可以将模式分为两类： 状态模式：对目标软件系统某部分的结构特征进行抽象，集中描述了该 部分的状态变量，并定义了这些变量之间的约束关系； 操作模式：对目标软件系统菜部分的行为特征进行抽象，通过描述操作 前后状态值之间的关系，定义了与若干状态模式相关的该部分的行为。 模式可以用阶谓词逻辑中的命题联结词连接，以构成新的模式。也可以通 过模式复合运算将多个操作按先后关系连接起来，构成一个完整的过程。 ( 2 ) 通用式及通用模式 在z 中存在一种特殊的常量，它以类型作为参数，被称为通用式( g e n e r i c ) 。 它可以当作模板为以后的变量声明所用。当通用式在其他变量的规格说明中出现 时，必须以实在的集合来代替它的类型参数，称为实例化( i n s t a n t i a t i o n ) 。模式的 通用式称为通用模式，这实际上是一种模板机制它的模式名称中含有形式参数， 这些参数是某些类型的子集。以不同的实参来实例化模板，则得到不同的模式。 ( 3 ) 公理描述 公理描述引入一个或多个全程变量和关于它们的谓词。这些变量不能是前 面已经定义的变量，它们的作用域从声明处至整个规格说明的结束处，它们的 限定i l i a 也具有全程的性质。 模式、通用式和公理描述是z 语言的基本构造单元，它们组成了z 的模式 语言，再加上数学语言如：一阶逻辑、集台、类型、关系、函数、序列和包等， 兰州大学硕士学位论文 u m l 建模的形式化研究 就构成了z 规格说明的主体。 2 2 3z 规格说明的结构 一个完整的z 规格说明由形式部分和非形式部分组成，在整个规格说明文档 中非形式的正文是伴随着形式规格说明出现的，起解释说明作用。一般说来， 一个z 形式规格说明文档的总体结构由以下几部分组成1 7 j = f 1 ) 给定集合、全程变量 给定集合和几个标准类型如整数、自然数等构成了规格说明类型的基础。 全程变量的定义在整个规格说明的作用域内是有效的，表达了全程的限制，一 般由公理描述给出。 ( 2 ) 系统的抽象：状态的描述 系统的抽象状态就是对客观世界的模拟，这种抽象状态的描述应该能识别 用来模拟现实世界中实际应用问题所使用的数据结构的重要部分。 ( 3 ) 系统合适的初始化的定义 系统初始化就是对系统的状态模式给出一个初始状态的描述，即对系统状 态模式中的一些变量赋初值。 ( 4 ) 在正常条件下系统的操作定义 有了系统的状态模式，就可以定义该模式下的一些操作。所谓“正常”的 条件是指该操作能成功执行的条件。 ( 5 ) 在可能出错的条件下的操作定义 ( 6 ) 操作模式的前置条件 操作模式的前置条件给出了该操作能成功执行的状态。 ( 7 ) 规格说明的些推理、证明 2 2 4z 语言的特点 能够用数学的方法对规格说明进行形式推理是z 相对于其它规格说明方法 的一个主要优点。另外z 语言具有简明性、易组合性、层次性和实用性等特征。 在书写系统规格说明时，可用来说明系统功能和顺序程序设计。但是，z 语言也 存在如下缺点_ 】： 兰州大学硕士学位论文 u m l 建模的形式化研究 o ) z 语言对大型系统的模块化能力不足 因为在z 语言中，目标软件系统的结构和特征都用模式来描述，随着系统 的增大，模式也会越来越多，而z 语言中没有更加有效的机制来管理这些模式， 最终导致z 规格说明难以阅读。 但) 难以识别影响某一状态模式的所有操作模式 因为在z 语言中，一个操作模式可能涉及多个状态模式，为了确定能影响 特定状态模式的所有操作模式，就需要逐个检查全部操作模式的声明部分，这 对于大型软件系统的规格说明来说是不实际的。 ( 3 ) 没有操作的时态次序，难以描述并发行为： ( 4 ) z 语言难以用计算机直接处理。 因为在设计z 语言时，只是考虑到把z 语言作为一种严格的描述手段，并 没有考虑到将来由计算机辅助进行z 语言应用，所以许多z 语言符号在计算机 中没有对应的键，难以进行规格说明的输入和自动化处理。 2 3z 的面向对象扩充o o z s 由于z 语言描述大型系统时模块化能力不强，而随着面向对象方法在系统分 析、系统设计和程序设计方面提出了新的技术和观点，尤其面向对象系统设计 方法中，提出了如类、层次、封装性和继承性等概念，对提高系统的模块性有 特殊的能力，有助于大型系统需求规格说明的编写和管理：另外，对象技术导 致复用，而程序构件的复用导致更快的软件开发和高质量的程序；面向对象的 软件易于维护，因为它的结构是内在松耦合的，这样当进行修改时，对整个软 件结构的影响较小；此外，面向对象系统易于进行适应性修改及伸缩( 即通过组 装可复用子系统而可以创建大的系统) 。因此，将z 和面向对象方法结合是zu s e r 最关心的问题。9 0 年代以来，国际上相继出现了多种z 规格说明语言的面向对 象扩展方案，其中较著名的有m o o z 9 1 ，o b j e c t - z t l o 】f 1 1 】，z 叫1 2 1 等。 基于“由规格说明建立一个快速原型”的思想，文献 1 3 1 4 中设计了一种 面向对象的形式规格说明语言o o z s ( o b j e c t o r i e n t e dzs p e c i f i c a t i o n ) ，以提高z 语言的结构化能力，支持大型软件系统的分析及其规格说明的书写，并使之能 直接在计算机中进行处理。 兰州大学硕士学位论文 u m l 建模的形式化研究 2 3 1o o z s 语法规则的形式 本文采用b a c k u s - n a u r 形式体系描述o o z s 的语法，它由组语法规则组成。 语法规则由非终结符、终结符和连接词构成，形为s ：= e 。它表示左边的s 被定 义为e 。其中s 为非终结符，形为 ，表示语法单位，汉字列是该语法单 位的名称；e 是语法表达式，形为t ljt 2l ft n ，表示e 可以为t 】或t 2 或t 。( 1 s i 9 ) 。 - 本文定义中用到的元符号及其语义如下： ：= 表示“被定义为”，用于各种语法单位的定义之中； 】表示括号里的内容可以不出现或出现一次； j 表示或。 2 3 2o o z s 常用的数据类型 o o z s 中出现的任何常量、变量、表达式有且仅有一种类型。o o z s 具有 两个基本类型，还可以让用户指定数据类型，并提供了一组从已有类型构造出 新数据类型的类型构造机制。此外，用户还可以自己定义“类”，这些“类”也 可以作为类型使用。本文中使用的数据类型主要有四种： ( ) 一 ( ) i ： p r e ( 谓词部分 l p o s t 月 e n ds c h e m a 2 3 5o o z s , 的类机制 z 语言中个操作模式可能涉及到多个状态模式，为了确定能够影响某特定 状态模式的操作模式，就需要逐个检查所有模式的声明部分，对于大型软件系 统的规格说明来说，这是不实际的。为了克服这个问题，o o z s 中限定“一个操 作模式至多作用于一个状态模式”。这样在o o z s 中，一个状态模式及作用于该 状态模式上的所有操作模式( 以及支持面向对象机制的其它概念) 就组成了类的 兰州大学硕士学位论文 u m l 建模的形式化研究 定义，其语法结构如下： ( 类定义) ：= c l a s s ( 标识符) ( 模板参数表) 】 ； 【s u p e r c l a s s ( 超类表) 】；1 o w l 2 s ( 常量定义) ；( 常量定义) ) ； ( 状态模式) e n do w n s ； 【i n i t ( 初始状态模式) ；】 m e t h o d s ( 操作模式) ；( 操作模式) ) e n dm e t h o d s ；】 【p r i v a t e ( 不可见表) 】；】 e n dc l a s s ； o o z s 中除了普通类之外还可以定义带有参数的类( 模板类) ，即在类定义 的标识符后面加上模板参数表，表中提供的模板参数在模板类中作为类型使用。 s u p e r c l a s s 子句中的超类表声明了类的超类，o o z s 语言支持多重继承，对所定 义的类，其直接超类需要在超类表中声明。o w n s 子旬定义了类的属性，包括状 态常量和状态变量。状态常量的值在对象生存期间保持不变，它们用一组常量 定义来描述；状态变量的值在对象生存期间可能发生改变，每个变量用一个状 态模式进行描述。初始状态模式i n i t 则定义了可能的初始状态。m e t h o d s 子句定 义了类的方法，它由一系列作用于类属性的操作模式组成。p r i v a t e 子句的不可 见表限制了类的属性和方法的使用，表中列出的属性和方法对外是不可见的。 2 3 6o o z s 规格说明 o o z s 规格说明的主体由一系列的类组成，这些类之间可以具有聚集或继 承关系。除了类之外，o o z s 规格说明还包括其它一些辅助部分，通常把这些部 分与类定义都称之为段落。 ：= ； 段落 ； ：= i n c l u d e “ ” a x i o m ； ) i ； 】 f o r w a r dc l a s s ， ) i ( 1 ) 文件包含：i n c l u d e “ ” 兰州大学硕士学位论文u m l 建模的形式化研究 使用其它文件中定义的类、常量或类型，实现规格说明的重用。 ( 2 ) 公理化定义：a x i o m ； ) 定义在本规格说明中要用到的常量，也可以在这里定义一些操作。 ( 3 ) 类型声明：g i v e n s e t ； ) 声明在本规格说明中要使用的类型名称，或定义自由类型。 ( 4 ) 前置声明：f o r w a r dc l a s s ， ) 对需要提前声明的类，在定义前声明其标识。 ( 5 ) 类定义 类定义中定义了类的内部结构。它是o o z s 规格说明的主体部分。 2 3 7o o z s 语言的特点 ( 1 ) 表达力强、简明直观：采用一阶谓词逻辑和集合论作为其形式语义基础， 把映射、函数等数学概念用到规格说明中来，简明直观，易于阅读；提供了较 强的功能描述设施，使用户可以用o o z s 书写完整的软件规格说明。 ( 2 ) 结构清晰、支持规格说明重用：o o z s 增加了“类”的概念，利用面向 对象中聚集和继承机制实现了规格说明的重用；规格说明的主体由一系列类组 成，结构化能力强，规格说明结构清晰。 ( 3 ) 提供入口、出口机制：o o z s 为操作模式提供了入口、出口机制，操作 模式通过入口和出口与外界进行信息交换，提高了z 语言的数据隐蔽能力，并 使其结构更加清晰。 ( 4 ) 设置了p r e 谓词和p o s t 谓词：o o z s 的操作模式中用p r e 谓词来描述操 作的前状态，用p o s t 谓词来描述操作的后状态。 因此，本文中采用o o z s 作为工具，建立起一种从u m l 模型到o o z s 规 格说明的映射。在此基础之上，可以很方便地将需求工程中建立的各种模型转 化为o o z s 规格说明，并进行必要的推理和验证，也可以进一步地从需求模型 自动产生测试用例。 兰州大学颤士学位论文 u m l 建模的形式化研究 第三章统一建模语言u m l 3 1u m l 的发展历史 公认的面向对象建模语言出现于7 0 年代中期。从8 0 年代到9 0 年代，其数 量从不到十种增加到了五十多种，出现了一大批优秀的方法，其中最引人注目 的是b o o t h 9 3 、o o s e 和o m t - 2 等。 b o o c h 是面向对象方法最早的倡导者之一，他提出了面向对象软件工程的 概念。他将以前面向a d a 的工作扩展到整个面向对象设计领域。b o o c h 9 3 比较 适合于系统的设计和构造。 r u m b a u g h 等人提出了面向对象的建模技术( o m t ) ，采用了面向对象的概 念，并引入各种独立于语言的表示符。该技术用对象模型、动态模型、功能模 型和用例模型，共同完成对整个系统的建模，所定义的概念利符号可用于软件 开发的分析、设计和实现的全过程，软件开发人员不必在开发过程的不同阶段 进行概念和符号的转换。o m t - 2 特别适用于分析和描述以数据为中心的信息系 统。 j a c o b s o n 于1 9 9 4 年提出了o o s e 方法，其最大特点是面向用例( u s ec a s e ) ， 并在用例的描述中引入了外部角色的概念。用例的概念是精确描述需求的重要 武器，它贯穿于整个开发过程，包括对系统的测试和验证。o o s e 比较适合支 持商业工程和需求分析。 面向对象建模市场的繁荣也带来了不少问题。首先，面对众多的建模语言， 用户很难找到一种比较适合其应用特点的语言i 其次，众多的建模语言实际上 各有千秋；第三，虽然不少建模语言大部分雷同，但仍存在某些细微的差别， 极大地妨碍了用户之间的交流。因此在客观上，极有必要在精心比较不同的建 模语言优缺点及总结面向对象技术应用实践的基础上，组织联合设计小组，根 据应用需求，统一建模语言。 1 9 9 4 年1 0 月，g r a d 3 jb o o t h 和j i mr u m b a u g h 开始致力于这一工作。在第 二年，o o s e 的创始人i v a rj a c o b s o n 加盟到这一工作。经过三人的共同努力， 于1 9 9 6 年6 月和l o 月分别发布了两个新的版本，即u m l0 9 和u m l0 ，9 t ，并 兰州大学硕= 匕学位论文u m l 建模的彤式化研究 将之命名为u m l ( u n i t i e dm o d e l i n gl a n g u a g e ) 。 u m l 的开发得到了来自公众的正面反应，1 9 9 6 年成立了u m l 成员协会， 以完善、加强和促进u m l 的定义工作。在诸多成员公司的共同合作下，u m li 0 诞生了。u m l1 0 是一个定义明确的、富于表达力的、强大的、应用于广泛问 题域的建模语言。 1 9 9 7 年1 1 月1 4 日，u m l1 1 被o m g 采纳。之后，对u m l 的改进工作 由o m g 接管，并产生了u m l1 2 ，1 3 ，1 4 版本。目前o m g 正在酝酿推出u m l 的2 0 版本。 3 2u m l 的概念模型 作为一种图形化的建模语言，u m l 的概念模型主要包含如下三部分内容： u m l 语义 支配u m l 的规则 运用于整个u m l 的公共机制 u m l 语义和语义表示法是u m l 定义的两个基本部分，分别由元模型和 图表示。图是u m l 语义的表示法，而元模型则给出图的语义。u m l 语义用于 对现实世界进行抽象和描述，而u m l 表示法则通过可视化的图形符号表达 u m l 语义。u m l 的规则用来将u m l 图形符号有机地组合在一起，并且保持 前后致。u m l 的公共机制提供了对u m l 详述、修饰和扩展等机制和功能。 总之，u m l 语义和表示法用于描述客观世界，而u m l 的规则和公共机制用于 约束和协调u m l 语言。 3 2 1u m l 语义的模型框架 u m l 的语义定义在一个四层的建模概念框架中，这四层分别是：用户对象 ( u s e ro b j e c t ) 层、模型( m o d e l ) 层、元模型( m e t a m o d e l ) 层和元一元模型 ( m e t a m e t a m o d e l ) 层( 见表3 1 ) 。 表3 1 中各层是采用类似递归的方式定义的。不同的层次模型表达不同层次 的抽象语义。u m l 语言自身被定义在元模型层上面，也就是通过元一元模型层 的模型元索来构造u m l 。作为元模型层次上的u m l 模型可以用来定义各种 兰州大学硕士学位论文u m l 建棋的形式化研究 u m l 模型的结构，从而，建模人员可以运用u m l 模型元素构造应用领域模型。 层描述示例 元模型体系结构的基础结构，定 元一元模型元类、元属性、元操作 义了规定元模型的语言。 元一元模型的实例，定义了规定 元模型类、属性、操作、构件 模型的语言 元模型的实例，定义描述某一信 模型学校、学生、课程、成绩 息域的语言。 模型的实例，定义了特定领域的 用户对象数据结构 值。 表3 ，lu m l 的四层模型理论 3 2 2u m l 的模型元素 u m l 模型元素也叫u m l 语义构造块，用来抽象、描述现实世界的u m l 语义成分，u m l 的词汇表包含三种模型元素：事物、关系和图。事物是对模型 中最具有代袁性的成分的抽象，关系把事物结合在一起，这两者通过u m l 的 图形符号表示出来。 ( 1 ) 在u m l 中有四种事物：结构事物、行为事物、分组事物、注释事物。这些 事物是u m l 中基本的模型元素，用它们可以构造结构良好的模型。 结构事物( s t r u c t u r e l h i n g ) 结构事物是u m l 模型中的静态部分，描述概念或物理元素。u m l 中共有 7 种结构事物：类、接口、协作、用例、主动类、构件、节点。其中类( c l a s s ) 是一组具有相同属性、相同操作、相同关系和相同语义的对象的抽象。接口 ( i n t e r f a c e ) 是描述一个类或构件的服务的操作集。协作( c o l l a b o r a t i o n ) 定义了一组 元素的交互，并且这些元素共同工作的行为大于各个元素独立行为的总和。用 例( u s ec a s e ) 是对一组动作序列的描述，系统执行这些动作将产生一个对特定的 参与者有价值的可观察的结果，用例是对系统提供的功能的描述。主动类( a c t i v e c l a s s ) 是至少拥有一个线程或进程，因而能启动控制活动的类。构件( c o m p o n e n t ) 是系统中物理的、可替代的部件。节点( n o d e ) 是运行时存在的物理元素，它表示 了一利，可汁算的资源。 行为事物( b e h a v i o r a lt h i n g ) 行为事物是u m l 模型的动态部分，描述了跨越时间和空间的行为。u m l 兰州大学硕士学位| 文 u m l 建模的形式化司f 宄 中主要有两类行为事物：交互和状态机。交互( i n t e r a c t i o n ) 由在特定的语境中共 同完成一定任务的一组对象之间交换的消息组成。状态机( s t a t em a c h i n e ) 描述了 个对象或一个交互在生命期内响应事件所经历的状态序列。 分组事物( g r o u p i n gt h i n g ) 分组事物是u m l 模型的组织部分。在所有的分组事物中，最主要的是包 ( p a c k a g e ) 。包是把元素组织成组的机制。 注释事物( a n n o t a t i o n a | t h i n g ) 注释事物是u m l 模型的解释部分，用来标注模型的任何元素。 ( 2 ) 在u m l 中的关系： 依赖( d e p e n d e n c y ) 是两个事物问的语义关系，其中一个事物( 独立事物) 发生变化会影响另一个事物( 依赖事物) 的语义，但反之则未必： 关联( a s s o c i a t i o n ) 是一种结构关系，它指明