UML顺序图与状态图一致性检验（可编辑）

UML顺序图与状态图一致性检验（可编辑） UML顺序图与状态图一致性检验 中山大学 硕士学位论文 UML顺序图与状态图一致性检验 姓名:汪胜 申请学位级别:硕士 专业:计算机软件与理论 指导教师:姜云飞 20090520中山大学硕士学位论文 论文题目:顺序图与状态图一致性检测 专业: 计算机软件与理论专业 硕士生: 汪胜 指导老师:姜云飞教授 摘 要 近年来,软件规模的不断扩大,复杂度不断增加,如何提高软件开 发效率, 保证软件的质量成为软件工业界的关键性问题。统一面向对象建 模技术为提高大 规模软件开发的效率与质量带来了希望,为软件开发自动化奠定 了基础。统一面 向对象软件建模语言以其图形化的表达及对软件设计提供各种各样的支持 而迅速成为软件业界的 标准 excel标准偏差excel标准偏差函数exl标准差函数国标检验抽样标准表免费下载红头文件格式标准下载 。开发人员可以使用多种角度对系统进行建模,但是 不同视图模型可能存在信息冗余,可能导致视图不一致性等问题。因此,对 进行形式化描述与研究,给出准确的形式化定义,可以提高该语言的准确 性、扩展性和一致性。 顺序图常用于描述并发系统的设计需求,着重体现对象之间消息传递 的时间顺序,因此,用一个适当的时序逻辑描述语言来给出它的语义是可行的。 /是一种可执行的线性时序逻辑语言,既可描述系统的动态行为又可表示 程序性质,对顺序图进行形式化规约后,可在统一的时序逻辑框架下 分析 定性数据统计分析pdf销售业绩分析模板建筑结构震害分析销售进度分析表京东商城竞争战略分析 顺序图 的性质。论文给出了一个改进的顺序图语法定义,同时对基于/时序逻辑 语言的顺序图语义进行了深入研究,针对存在的问题,根据给出的语法定 义,提出了新的解决 方案 气瓶 现场处置方案 .pdf气瓶 现场处置方案 .doc见习基地管理方案.doc关于群访事件的化解方案建筑工地扬尘治理专项方案下载 ,更加精确地描述了顺序图的语义。 本文主要是对具有多种逻辑语义的顺序图提出语义分析方法,为复杂层次结 构的状态图引入自动机,应用自动机算法得到自动机树,同时制定了新的顺序图 与状态图的一致性检测准则,用模型检验工具对顺序图与其相关的状态图 进行一致性检测。 关键词:统一建模语言、模型检测、时序逻辑语言、一致性检测中山大学硕士学位论文: : : : , . . . .,, . . , .,., , .’ . ./,./, . /. ? , ,中山大学硕士学位论文 . . , .. . : , / , 论文原创性声明 本人郑重声明:所呈交的学位论文,是本人在导师的指导下,独 立进行研究工作所取得的成果。除文中已经注明引用的内容外,本论 文不包含任何其他个人或集体已经发表或撰写过的作品成果。对本文 的研究作出重要贡献的个人和集体,均己在文中以明确方式标明。本 人完全意识到本声明的法律结果由本人承担。 学位论文作者签名:.?堡母趁 日飙乒严 学位论文使用授权声明 本人完全了解中山大学有关保留、使用学位论文的规定,即:学 校有权保留学位论文并向国家主管部门或其指定机构送交论文的电 子版和纸质版,有权将学位论文用于非赢利目的的少量复制并允 许论 文进入学校图书馆、院系资料室被查阅,有权将学位论文的内容编入 有关数据库进行检索,可以采用复印、缩印或其他方法保存学位论文。 学位论文作者签名:汐 导师签名勘 导师签名瓤。眨 醐:叶朔啪 嗍:朋地日中山大学硕士学位论文 第一章绪论 .背景介绍 传统的系统分析和设计存在很多不足,如开发出来的软件与实际需求不符、 维护困难、软件的复用率低等。为了解决这一系列的问题提高软件设计质量及鉴 于软件质量问题的重要性和迫切性,人们提出各种方法和技术来提高软件质量, 软形式化方法、面向对象方法及软件测试等技术。其中形式化方法研究严密的数 学为基础,使人们能够以精确的方法来表示概念证明规范和设计的性质,并且在 开发出软件产品之前就能对产品的行为进行推理。经过多年的计 算机科学研究和 工程 路基工程安全技术交底工程项目施工成本控制工程量增项单年度零星工程技术标正投影法基本原理 实践,人们已经认识到形式化方法和技术是提高系统可靠性和质量的重要途 径。自世纪年代中期以来,高可信软件和系统受到了国际上的广泛重视, 成为计算机科学技术的重要热点。然而,?如何开发高可信软件己成为国内外软件 界一个非常棘手的问题。人们普遍认为,目前的软件技术水平已无法满足高可信 软件的开发需求在我国国防建设实践中,科技强军对军用软件也提出了高可信的 需求,急需发展可信软件工程技术例如,载人航天的软件工程、先进武器的软件 工程和软件工程等许多重大任务都对软件的可靠安全性的保障提出了迫切 需求。 在形式化方法中,模型检验 是一种很重要的自动分析和验 证技术,其实质是利用计算机的快速计算能力,通过穷举被检验系统的有穷状态 空间中的每一个状态来验证该系统是否满足特定的形式规约。相对于传统的形式 化证明方法而言,模型检验方法具有快速、全自动、对使用人员的数学背景要求 ‘ 不高的特点。很多情况下,可以把模型检验和各种抽象与归纳原则结合起来验证 非有穷状态系统如实时系统。模型检验己经在硬件电路、 协议 离婚协议模板下载合伙人协议 下载渠道分销协议免费下载敬业协议下载授课协议下载 验证、软件系统 规范与分析中得到成功的应用,例如标准的验证、各种协议验证、大型通 讯软件验证等。 近年来,在组织和各大厂商的推动下,作为工业标准的统一建模 语言 得到了极大发展。过程受到了广泛的关 中山大学硕士学位论文 注,已经成为面向对象建模的事实标准。提供了多种建模提供了多种 建模机制,从不同角度和应用层次刻画系统的特性和复杂的运行环境,为软件开 发入员提供从系统需求分析、设计到实现的有力支持。但是,自身也存在一些缺 陷,其中规范使用较为形式化的语言即对象约束语言和自然语言两种手段描述静 态语义,而动态语义基本上完全用自然语言来描述。采用这种方法描述的动态语 义,存在着不完全、不一致、模糊性等缺陷,难以支持对复杂系统的模型进行严 格的语义分析和正确性验证。因此形式语义的研究,对增进该语言的清晰性、一 致性、可扩展性是十分有帮助的,为模型的正确性证明、转换以及支持的建模工 具的一致性检查提供有力的理论工具,但这种具有空前复杂性的建模语言 是否能有成效的形式化仍是一个问题。 .研究现状 软件形式化方法最早可追溯到世纪年代后期对于程序设计语言编译技 术的研究,即.提出描述语言的语法,出现了各种语法分 析程序自动生成器以及语法制导的编译方法,使得编译系统的开发从“手工艺制 作方式”发展成具有牢固理论基础的系统方法。形式化方法的研究高潮始于 世纪年代后期,针对当时所谓”软件危机。形式化方法的基本含义是借助数学 的方法来研究计算机科学的有关问题,是基于数学的方法来描述 目标软件系统性 质的一门技术,用严格的数学符号和数学法则来对目标系统的结构和行为进行有 效的综合、分析、推理。它为系统的说明、开发和验证提供了一个框架,有利于 发现目标软件系统中的不一致、不完备等方面。人们提出种种解决方法、归纳起 来有两类:一是采用工程方法来组织、管理软件的开发过程;二是深入探讨程序 和程序开发过程的规律,建立严密的理论,以其用来指导软件开发实践。 形式化方法的一个重要研究内容是形式规约 也称形式 规范或形式化描述,它是对程序“做什么 的数学描述,是用具有精 确语义的形式语言书写的程序功能描述,它是设计和编制程序的出发点,也是验 证程序是否正确的依据;形式验证形式化方法的另一重要研究内容是形式验证 ,形式验证与形式规约之间具有紧密的联系。证明一个程序 中山大学硕士学位论文 的正确性即程序验证。形式规约方法包括了各种基于数学的表示 法、语言以及 对应的工具,形式验证方法包括各种模型检查器、定理证明器等实验的方法对系 统进行查错。 .形式规约 形式规约的方法主要可分为两类:一类是面向模型的方法也称为系统建模, 该方法通过构造系统的计算模型来刻画系统的不同行为特征;另一类是面向性质 的方法也称为性质描述,该方法通过定义系统必须满足的一些性质来描述一个系 统。不同的形式规约方法要求不同的形式规约语言,即用于书写形式规约的语言 也称形式化描述语言,如代数语言、、、 /等:进程 代数语言、、?演算等:时序逻辑语言、、/、、 等;这些规约语言由于基于不同的数学理论及规约方法,因而也千差万别, 但它们有一个共同的特点,即每种规约语言均由基本成分和构造成分两部分构 成。前者用来描述基本原子规约,后者把基本部分组合成大规约。构造成分 是形式规约研究和设计的重点,也是衡量规约语言优劣的主要依 据。 .形式验证 形式验证与形式规约之间具有紧密的联系,形式验证就是验证已有的程序 系统,是否满足其规约‘,、,的要求即,、,,它也是形式化方法 所要解决的核心问题。传统的验证方法包括模拟和测试,它 们都是通过实验的方法对系统进行查错。模拟和测试分别在系统抽象模型和实 际系统上进行、~般的方法是在系统的某点给予输入,观察在另一点的输出,这 些方法花费很大,而且由于实验所能涵盖的系统行为有限,很难找出所有潜在 的错误。基于此,早期的形式验证主要研究如何使用数学方法,严格证明一个程 序的『确性即程序验证。 是一种定义良好、易于表达、功能强大且普遍适用的建模语言,它溶 入了软件工程领域的新思想、新方法和新技术。它的作用域不局限于支持面向对 象的分析与设计,还支持从需求分析开始的软件开发全过程由于复杂系统的建模 往往需要进行严格的形式化分析和验证,而却是半形式化的。 因为其语法结构虽然采用了形式化的规约,但其语义部分则是用自然语言描 述的,缺乏准确的语义,这使得对模型难以进行定量定性的分析和验证。针对这中山大学硕士学位论文 一问题,形式化方法的研究已经成为热点。形式化方法使用具有精确数学语义基 础的形式化规范语言对系统的需求分析、设计进行描述,它具有精确定义的语义 模型、自动化验证工具的支持,可以对软件规范进行严格的分析和验证。目前, 许多学者在的形式化方面进行了大量的工作,从形式化技巧的角度来看,这些方 法大致可以分为两类: :用模型定义形式化语义,在此基础上对模型进行语义分析和正确 性验证。 由于形式化方法需要设计者具有很好的数学基础,这使得直接使用形式化规 范对系统,尤其是大型的复杂系统建模时难度很大,而该类方法正是直接给模型 定义形式化语义,然后使用具有严格形式化语义定义的进行建模,因此这类方法 应用起来并没有克服形式化方法所固有的缺点。文献给出一组和相对 应的数学模型,文献【】定义了一种包含对象流描述的活动图的形式语义,文献【】 给出了状态机的组合操作语义。 :结合跟形式化方法的优点。将非形式化的图形转换为具有精确语 义定义的形式化规范,在非形式化的图形表示与形式化定义之间建立映射关系。 该方法主要是应用图形方法建模,将形式化的描述用于建模的分析、 验证,它对一般的用户是透明的,因此避免的形式化方法的局限性,并且克服了 缺少模型分析和验证手段的不足。 形式化方法在软件设计与开发中起了重要的作用。形式化方法描述给软件的 开发的需求分析提供明确性、一致性的描述,而那些非形式化描述很可能导致描 述的不明确和不一致。形式化方法则要求描述的明确性,而描述的不一致性也就 相对易于发现其次是对软件设计的描述,软件设计的描述和软件要求的描述一样 重要。形式化方法描述软件要求的优点同样适用于软件设计的描述。另外由于有 了软件要求的形式化描述,我们可以检验软件的设计是否满足软件的要求。对于 编程来讲,我们可以考虑自动代码生成。对于一些简单的系统,形式化的描述有 可能直接转换成可执行程序,这就简化了软件开发过程,节约了资源和减少了出 错的可能性。另外,形式化方法可以用于程序的验证,以保证程序的正确性。对 于测试来讲,形式化方法可用于测试用例的自动生成,这可以节约许多时间和在 一定程度上保证测试用例的覆盖率。中山大学硕士学位论文 虽然形式化方法在软件工程级其他计算机领域取得的很大的成功,但是跟面 向对象技术和相比其实用性还是存在很大差距。其主要问题在: .软件开发过程跟形式化方法难以平滑的结合。 .形式化方法主要是以代数理论、计算逻辑和软件结构为基础。因此在实 质上是一种严格的、灵活性较差的方法,缺乏必要的实施手段和支持工具,所以 难以在实际软件开发中被广泛的接受。 .形式化方法在解决小规模的问题是较为有效,却很难应用于大型的软件 开发。至今还没有一种形式化方法对软件开发的各个阶段提供全面的支持。缺少 有效的手段必然会限制形式化方法的发展。 .论文的研究方法 虽然在高可靠软件开发工作中得到了广泛应用,而且模型为高 可软件的可靠性确认和验证提供了丰富的信息,但是模型并没有直接支持 高可靠性软件可靠性确认和验证。然而运用可视的手段对目标系统进行建模,易 于理解的图形方式刻画和描述软件系统所包含的内容,并力争图形化跟形式化的 方法相结合,形成可视形式化的需求规范或设计规范提高软件建模的准确性和可 靠性。 随着的广泛应用,基于的建模工具在大型软件开发中得到越来 越多的重视。然而为了提供对其正确性、规范性验证,判断软件是否满足某些关 键的性质显得越发重要和迫切。为了提高软件设计的规范性并得到可靠的完善的 验证本文主要研究以下几个方面: ..顺序图的/时序逻辑语义研究,以及讨论模型的一致 性。 .对.顺序图与状态图的一致性研究并讨论模型检测,最后给出 的顺序图与状态图的一致性检测。中山大学硕士学位论文 .论文的组织结构 论文的组织如下: 第一章绪论,主要介绍以及形式化方法的研究背景、研究现状。 第二章主要研究.顺序图的时序逻辑语言/研究性,并提出一 个改进的顺序图语法定义,能更全面的描述顺序图的组成元素。然后,讨论顺序 图的形式化语义和语义的二义性,着重讨论基于/时序逻辑语言的顺序图 语义描述方案,针对其存在的问题,在给出的形式化语法定义的基础上并提出新 的解决方案。 第三章主要介绍.形式化研究,介绍语言体系结构,对 一致性问题的原因、分类、检测方法进行分析讨论。 第四章顺序图与状态图一致性研究与检测首先,介绍形式化模型检验 方法的原理和特点,并着重介绍模型检验工具的原理和语法。其次,提出 一个更全面的状态图语法定义,并针对复杂层次结构的状态图, 引入有限状态自 动机,提出自动机分解算法,经分解后得到自动机树。再次,提出对具 有多种逻辑语义的顺序图的分析方法,给出新的语义定义。最后,提出新的顺序 图和状态图的一致性检查准则、代码结构,以及将状态图转换成 代码的算法,并用模型检验工具进行顺序图和其相关状态图的一致 性检验。 第五章结束语,对全文进行总结,给出今后进一步的研究方向。 中山大学硕士学位论文 第二章.顺序图时序逻辑语言/的研究 .形式化方法与规范语言 现在的软件开发过程通常是,需求分析后进行体系结构设计,再逐步过渡到 最后的实现。无论开发过程中不同阶段能否交错,整个过程是否迭代,每个阶段 都由相应的文档记录。因此描述同一系统的各阶段文档应当保持一致。为了记录 每一步的工作内容,各种软件工程方法都提供了相应的语言机制来描述阶段信 息。例如结构化方法中用数据流图、数据字典等来描述需求相关 的信息,例如结 构化方法中用数据流图、数据字典等来描述需求相关的信息,用结构图来描述系 统结构包含哪些模块,模块间的调用关系,以及用于详细设计的图、伪 代码等;而面向对象的方法在多年的发展后形成了统一建模语言 及软件体系结构设计中常用的一些体系结构框图。这些工 程中常用建模语言的特点是:直观、半形式化、一般是图形语言、为广大软件开 发人员所熟悉,但是缺乏精确的语义,一方面在交流时容易引起误解,另方面也 难以分析。在这一点上形式化方法可与之互补。形式化方法的目的就是提供描述 手段以精确、无二义地描述系统,并提供分析手段以证明系统正确性。所以在软 件开发过程中,开发者通常将软件工程中的常用方法直观的图形建模与形式化 方法严格的语义及验证的相关技术相结合应用于软件开发过程,并且仍然保持 工程建模语言直观易用的特点。规范语言是计算机界为更直观、更精确地表示程 序“做什么”而提出的~种能够抽象描述系统行为的语言,用于描 述程序的语义。 典型的规范语言有、、/自动机等 .时序逻辑语言/的简介 时序逻辑存在一个很重要的特点,即它除了可以作为一种性质描述语言,通 过口令等时序算子刻画系统静态规范静态语义外,还可以通过下一时刻算子中山大学硕士学位论文 表示系统状态转换的概念。从而可以作为一种系统描述语言刻画系统动态行 为动态语义的变化过程显然,采用同一种语言既作为系统的性质描述语言又作 为其刻画语言,对系统的正确性分析具有优势。时序逻辑语言是基于 命题线性时序逻辑系统,将时序逻辑算子溶入程序设计语言中,使 其既可以作为一个逻辑系统也可以作为~个程序设计语言。/表达方式与 普通高级语言相似,易于为工程师和程序员所接受。同时,作为一种形式化语言, 它既可表达以前后断言及递归函数为特征的静态语义,又可表达以状态转换为特 征的动态语义,所以其中的变量类型也分为两个层次,上层为逻 辑型,用于表示 逻辑公式,下层为非逻辑型,用于表示常见高级语言中所有在表达式中出现的各 种类型。非逻辑型中的基本类型包括整型、字符串型、文件型、布尔型,还扩充 了浮点型、集合、枚举集、列表等,还有一种特殊的名字型变量。以名字为值变 量类型是控制类型,在/中有个非常重要的控制变量,其值为一个标号。 /将状态转换机制引入线性时序逻辑,有如下特点: 以统一的程序框架既表示程序的动态语义即状态转换机制如赋值、转 移等,又表示其静态语义即前置断言与后续断言规范。 语言的定义足够精确和形式化,而又不要求使用者除了通常的编程知识 外有更多的数学训练。~方面保证其功能与常见语言一致,另一方面又保证其理 论上的可靠性,而且表示语义的语言与常见程序语言的风格完全一致。/ 是一系列化语言族,它的最基本特征是以统一的框架,既能表示适应冯?诺依曼 体系的状态转换机制的命令式语言,又能表示程序逻辑推理特征 的直言式公式语 言。从这个角度划分,/分为两个子语言:满足前者的称为可执行/ 或/ /;满足后者的称为抽象觋或/ /。 ,。 /又根据控制结构的不同分为三个子语言:一种用直接表示状态转换 的命令形式控制结构的基本/或称/ /;一种用结构化 高级语言的语句形式控制结构的结构化/或称/ ; 一种用产生式规则形式控制结构的产生式规则型/或称//。在不同的控制结构中,既可以用可执行形式也可以用抽象形 式,所以这两组不同标准划分的子语言又可正交成六种子语言表.。 中山大学硕士学位论文 表. /六种子语言 / / / 不同 \ 一云 / / / / / / / / . /连接词及时序算子 /是线性时序逻辑语言 ,简称的一种 变型,线性时序逻辑是以一阶逻辑为基础,在线性时间序列上解 释语义的模态逻 辑,常用于描述反应系统的性质。常用的链接词如表? 表/的链接词 连接词 含义 符号表示 否定词 非 人 合取词 与 析取词 或 不可兼析取词 异或 ’ 一 蕴含词 蕴含 等值词 等值 全称量词 所有 存在量词 存在? 了 /包含有将来时序算子和过去时序算子,但/语言一般只用到将 来时序算子。过去时序算子的实现效率很低,故不作介绍。其将 来时序算子如表 所示。 中山大学硕士学位论文 表 /将来时序算子 将来时序算子 符号表示 下一时刻算子 必然算子 口口 终于算子 ?? 直到算子 除非算子 . /基本命令格式 /最基本的特征是在统一的时序逻辑框架下既能表示适应冯?诺 依曼体 系状态转换机制的命令式语言如?式,又能表示适应逻辑推理特 征的直言式公 式语言如?式。 ? 之? 式??是/中的基本命令形式,称为条件原子式,或简称条件元 其中“”表示下一时刻算子或终于算子?;、为一阶逻辑公式: 称为条件元的动作部分。是蕴涵词一在 称为条件元的条件部分;和 条件元这一语言层次的特殊表示形式;标号与分别为条件元的定 义标号与转 出标号。其实式?是将式?的动作部分进行扩展,将并行赋值等 式包括在 中。正中的输入输出有以下几种方式,如表所示。 表 /的输入输出命令 输入命令 、 ? 、? 输出命令 其中和是/的通道命令,是通道名。输入命 令从通道或终端接收输入数据后,由输出命令输出到另一个通道 或者终端。 中山大学硕士学位论文 . 顺序图的基本语法与语义 .. 顺序图的语法 顺序图属于交互图,交互图是系统的动态视图,包括对象和它们的关 系,以及对象之间相互传递的消息。顺序图强调消息传递的时间顺序,展 示对象在其生命线上参加的交互它们按时间顺序交换的消息,它所展示的是一组 在对象之间为产生所要求的操作或操作结果而进行合作时相互交换的一组消息。 顺序图是为系统建模的主要工具。它尤其适用于面向对象的软件,在对象 交互是表示其控制流,顺序图表示了一系列的交互对象和交互对象问消息交换的 传 顺序。它还可以包含一些额外的信息如:如 一卜. “ 递”和迭代“传送消息次和状态依赖行为等。它显示了参与对象,而不 是刻画对象间的关系或对象的属性。本文在研究文献提出的顺序图语法定义 的基础上给出如下改进定义。 定义. 顺序图 顺序图是一个四元组,,,,其中: .,?..,,是顺序图中算有对象生命周期上的时间点集合,代 表了消息发送和接收的顺序。在每一个时间点上配置了一个标记 函数 ,?,,,,,,,,,,,, ,,意思是在时间点,对象发送了一个消息,以此类推, 代表发送消息的反馈,代表接收消息,代表接收消息的反馈, 代表可选片断,代表循环片断,代表选择片断,代表断言片断, 代表否定片断,代表弱序片段,代表严格序列片断,代表跳出 片断,代表临界片断,表临界片断结束,代表并发片段。 .,?..,是顺序图中所有对象的集合。每个对象都是某个 类的实例,用标志所属类名。在每个对象的生命周期中有一组 时间点集合。,记,..?,,它是总时问点集合的子集, .。.中任意的‘和‘,那么,那么,只。在‰之前 出现。中山大学硕士学位论文 .,,..?,是顺序图中国所有消息的集合。每个消 息是一个七元组:,,:,,,, ,其中: 是发送消息对象,是类的实例 是接收消息对象,是类的实例 是类和类之间的关系 是调用的方法,如果,那么是的 自身方法调用 是消息的发送事件 是消息的接收事件 是此消息所属的域,可以是整个顺序图,或顺序图的某个组合片 断, 甚至是嵌套在组合片断内的某个组合片断 .,,..?,。是顺序图中所有组合片 的集合,每个组合片段是个五元组: ,,,,,其中: 是该组合片段的交互操作符,其值为?、、、、 、、、、、 是该组合片断覆盖的生命线集合 是该组合片断所包含的消息集合 是该组合片断内所嵌套的组合片断集合,若无嵌套,则为空 是该组合片断包含的交互操作集合,当为、、、 任意一个时,组合片断只能包含一个交互操作 .顺序图中最主要的新增核心构造物是组合片断,定义扩展了一 个新 的元素,专门用于定义顺序图中包含的所有组合片断。每个是一 个五 元组,由交互操作符、生命线集合、消息集合、子片断、交互操 作集合组成,非 常全面的包含了组合片断中所有的组成元素。同时还扩展了标记函数中的组合片 断类型。与己有的研究相比,该定义能更精确的描述顺序图.。 中山大学硕士学位论文 ..顺序图的语义 .问题陈述 文献【】同样采用/来描述顺序图的语义,其思想是将.顺序图 的组成元素映射为/的条件元转换: : 其中表示组成元素的集合,表示/条件元素。基于映 射,对每个组成元素,根据不同情况,它的条件元定义如下所示: 如果?,即元素为消息类型,则 . 为/中的一种转出标号,代表下一个条件元的定义标号,如果条件元 是它所在单元的最后一个条件元,则转出标号用表示。如果 .,即组合片段的交互操 作符为,则八 其中,?表示此组合片段内的交互操作,?.表示执行某 个交互操作应该满足的条件,并且: ,...,,?:. 如果?.,即组合片段的交互操 作符为,则八 八。 如果?.,即组合片段的交互操 作符为,则 【??】 如果?.,即组合片段的交互 操作符为,则 【??】中山大学硕士学位论文 如果?.,即组合片段的交互操 作符为,则 【 .?. 如果?.,即组合片段的交互 操作符为,则 八薹 八~兰兰 其中和分别表示执行循环要满足的最小值和最大值,为交互操 作。 如果.,即组合片段的交互 操作符为,则上述方案存在以下几个问题: .顺序图的语义是基于事件序列的,,??.,?,., 为消息的发送事件或接收事件。如图.,这是一张最简单的顺序图,只包含 一个消息,这个消息有两个事件,在的生命线上发生的发送消息事件,用 表示,在的生命线上发生的接收消息事件,用表示,消息的发送事件必须 一先于接收事件。该顺序图语义即:,。 图.最简单的顺序图 .顺序图的消息默认为偏序关系,也就是弱序列。 定义..弱序列多个消息之间是弱序列关系,必须满足一下三个条件: 中山大学硕士学位论文 消息执行的最终结果是不变的; 同一生命线上的不同消息事件按照先后顺序依次发生; 不同生命线上的不同消息事件可以按照任意顺序发生。 图.弱厅歹 图.显示了一个顺序图包含两个消息,都是从指向,语义为: .【,协,妒 ,,,,,,, 消息的发送事件必须第一个产生,但是之后可能是消息的发送事件,也 可能是消息的接收事件。消息和的接收事件分别在各自的发送事 件后发生。 图.含临界片段的顺序图中山大学硕士学位论文 图.显示了一个顺序图,其中包含一个临界片段和一个消息,其语义为: 《‘【,。》 ,‘政,,,,,, 文献【】对组合片段的描述与.规范中的定义不符合,它将 组合片断描述为交互操作的并发,但是正确的理解应该是组合片段内的消息满足 弱序列约束。 文献【】对组合片断的描述只表达到交互操作的并发,未细化到时间 层,而顺序图的语义是由事件序列组成的,而且组合片断的各个操作内的消 息必须满足弱序关系。如图.显示了一个顺序图,包含并发组合片断,其语 义为: ,, ,,;,,,,,,,,吼,,强,,,吼,, ,【, 图.带并发组合片段的顺序图 文献【】对组合片断的描述忽视了对条件片段的判断。 .改进的顺序图语义描述方案 根据以上分析,针对存在的问题,本文提出行的语义描述方案,如 下所示。 定义..顺序图组成元素的转换映射 中山大学硕士学位论文 .顺序图的组成元素到/的语义转换是~个映射。 : 其中表示组成元素的集合,表示/条件元素。 定义.. 顺序图的转换映射.顺序图到/的语义转换是一 个映射 :?》 其中,是顺序图集合,是/单元集。 若顺序图,,....,,则 八其中??分别表示对与??.,相应的条件约束。 根据前面的的顺序图语法定义,其中组成元素是对象、消息、组 合片段、“时 间点。下面我们在定义.顺序图组成元素的/语义的基础之上,给 出.顺序图的/的语义。 基于映射,对于没一个组成元素,根据不同情况,它的条件定义 如下所示: 如果?,即元素为消息类型,则 八..八 为/中的一种转出标号,代表下一个条件元的定义标号,如果条 件元是它所在单元的最后一个条件元,则转出标号用表示。 如果?.,即组合片断的交互操作 符为,则八 八 . 其中,??表示此组合片断内的交互片断,,??,表示执 行某个交互片断应该满足的条件,并且 ’哟。 中山大学硕士学位论文 如果?.,即组合片段的交互操 作符为,则 八 八其中表示此组合片断内的交互片断,为执行应该满足的条件。 如果?.聊瓯即组合片段的交互操 作符为 ..,..,...,..,.. ,...,..,..,......,..】 ??. 其中;为并发合片断中的交互操作,每一个内的消息符合弱序关 系。 如果?.,即组合片段的交互操 作符为,则 ..,..,....,.,.. ‘】 其中为交互操作,是连续符号。 如果?.,即组合片段的交互操作 符为,则 .,.,?,,,. . . ?, ....?.一.. . 的?.. .? 其中为交互操作,为交互操作内的消息,..表示信息 的某个时间所在的对象生命线,..表示 的发送事件一定在的接收事件之前完成。 .,即组合片段的交互 如果 中山大学硕士学位论文 操作符为,则 八耋三八~兰耋 其中和分别表示执行循环要满足的最小值和最大值,表示这个组 合片断内要执行的交互操作。 如果?.,即组合片段的交互操 作符为,则 若存在条件则 若不存在条件则 .实验 ..实验描述 例如顺序图.描述的是一个集中式聊天室系统用户登录的场景, 由聊天者 ,客户端,服务器三个对象组成。用户输入用户名和密码给客户 端,客户端发送给服务器端进行验证,若是合法用户,客户端启动 聊天者初始化 功能,若是非法用户,返回登录失败信息。其语义为: ,,, ,,, ,, ,,, ,, ,, ,, ,, ,, , ,,,,, ,,,, ,,,, 中山大学硕士学位论文 ,, ,, ,, ,, 图.用户登录的场景顺序图 根据本文提出的定义和描述方法,它的/语义如下: ; 口 , . ; . . ;. . 八 ;; 八 : 八~ 】 : 口【中山大学硕士学位论文 . 【 ., ; .,.,.】 . . 八. . . . . .;】 .. : ;....; .. ..实验分析 图中有个组合片断,如果用文献【】的方法进行描述,其语义为: : ; ; 】 : ;。’; ; 】 ; ; 八 ; 】 和上节中用本问题出的描述方法相比,可以明显看出文献【】忽 略了组合片 断的交互操作默认为弱序列。并且文献【】将组合片断描述为交互操作的并 中山大学硕士学位论文 发,但是正确的理解应该是组合片断内的消息满足弱序列的约束。因此它不能正 确的描述组合片断。 .本章小结 顺序图经常被用于描述并发系统的设计需求,提供系统的正常执行场 景和异常执行场景。它描述对象之问的动态交互关系,着重体现对象之间消息传 递的时间顺序。它只显示参与的对象,而不刻画对象问的关系或对象的属性。 语法结构虽然采用了形式化的规约,但其语义部分则是用自然语言描述的, 缺乏精确的语义定义,这使得对模型难以进行定量定性的分析和验证。形式化方 法使用具有精确数学语义基础的形式化规范语言对系统的需求分析、设计进行描 述,它具有精确定义的语义模型:自动化验证工具的支持,可以对软件规范进行 严格的分析和验证。 顺序图新增了一些新的核心构造物,针对这些新特性,在分析了己有 顺序图语法定义的基础上,本文提出了一个改进的语法定义,更全面详细的描述 了顺序图的各种组成元素。随后,介绍了顺序图形式化语义的研究现状,讨论了 和这两个组合片断的二义性。详细分析了基于甩时序逻辑语言的顺序图语义,指 出其存在的问题,如忽略了顺序图中消息默认为偏序关系对组合片断的描述不符 合顺序图规范文档的定义语义定义未细致到事件层等。针对这些问题,根据上文 给出的语法定义,提出了新的用尼时序逻辑语言描述的顺序图语义,该方案能够 更精确的表达顺序图的语义。中山大学硕士学位论文 第三章形式化研究 面向对象建模语言出现于年代中期,面向对象的分析与设计方法的发展 在年代末至年代中出现了一个高潮,涌现出了一批新方法,其中最引人注目 的是 、和。在众多的建模语言中,语言的创造者大力推 崇自己的产品,并在实践中不断完善。但是用户并不了解不同建 模语言的优缺点, 很难根据应用特点选择合适的建模语言。不仅统一了、和 的表示方法,而且在此基础上有了进一步的发展,并最终形成大众所接 受的标准建模语言。 一些机构将作为其商业策略己日趋明显,的开发者得到了来自 公众的正面反应。参与制定标准的成员包括、、、、 . 以及等许多国际知名的机构和企业。 . 语言体系结构 .. 四层元模型体系结构 是个基于四层元模型结构,包括用户对象、模型、元模型、和元一元 模型四个层次。具体如下: 元一元模型. ,:元模型系统结构建模的基础结构,定义 了说明元模型的语言,例如元类 、元属性 、元操 作 都属于该层。该层通常用表示。其主要职责是定义一种 语言来描述一个元模型,就是一个元一元模型的例子。元一元模型通常比 元模型的描述更简洁,而且通常定义多个元模型。 元模型 ,:元一元模型的实例,定义了一个说明模型的语 言,例如类、属性、操作、组件 等都是属于该层。该层通常用表示。其主要职责是定义一个用于描叙模型的 语言,和的 模型都是个元中山大学硕士学位论文 模型的例子。元模型通常比用来定义它们的元一元模型描述的更加详细,尤其是 当它们定义动态语义时。元模型是的一个实例。 模型,:元模型的一个实例,定义了一个描述信息领域的语言。 该层通常用表示。其主要职责是用来定义描述各领域语义的语言,例如允许 用户对各种不同的领域问题建模,如软件、商业过程以及需求等。一个用户模型 是元模型的一个实例,这个用户模型既包括模型元素也包括这些模型元素 实例的简要说明。 用户对象 场,:模型的一个实例,定义了一个特定的信息领 域。该层通常用表示。它包含运行时模型中定义的模型元素的实例,那些定义在 层中的简要说明被用于对层运行实例的约束。 当多于三个元层时,该体系结构中位置越是靠上的层,其描述会越简洁,其 规模会越小。以为例,它处于层,只是在中定义了一些元类。 在建立元模型时,有一个特殊的地方是关于定义语言的反射特性, 即语言可以被用来定义自身。中的臣就具有这样的特性, 它包含了定义自身所需的所有元类。当一个语言是反射的,就不需要再定义其他 语言来描述其语义。因为是基于丘 的,所以是反 射的,因此不需要在上构建其他元层。 ..存在的问题 规范中说,它的元模型是从抽象语法、良构规则、语义三个视角,用 半形式化.的方式来描述的,三者分别定义的语法、静态语 义和动态语义。 在形式化语言研究领域,迄今大部分成果和成熟技术是关于严格的形式化描 述的。衡量一种语言是不是形式化的,关键在于它的语法是不是采用严格的形式 化描述。至于语义的描述则允许是非形式化的。 的抽象语法是一个由的子集所描述的模型,其中包括类图 和“支撑自然语言”描述。对的每个包,规范使用一个或多个类图来表 示其中的各种构造物以及它们之间的关系,然后用大量的自然语言文字进行解 释,如此定义每个包的抽象语法。除此之外,目前用于描述语言语法的各种形式 中山大学硕士学位论文 化手段例如巴克斯范式、一乔姆斯基变换文法、自动机等等都没有采用 由于存在自然语言的描述,上述元一元模型和元模型都不是形式化的,用前 者描述后者也不像在形式化语言领域用一种元语言定义一种形式化语言那样严 格。因为元模型是一个逻辑模型而不是物理或实现模型,它强调语义 陈述而隐藏实现细节。需要定义类、属性、操作、关联、泛化、活动、状 态等一大批面向对象建模概念的语义,其他元模型例如接口描述语言也 有这样的需要。因此,作为这些元模型共同基础的元一元模型就在更高的层次上 定义了陈述这些概念所需的基础概念。元模型只是在用自然语言 陈述 自己提供的建模概念时引用元一元模型的概念,使其陈述显得较为精确。但是并 不是像一种真正的形式化语言那样,完全依靠一种形式化的元语言来定义整个语 言。规范称这种定义方式为“松散的非严格的元模型建模,即级 模型是级模型的一个实例。它所谓的“严格”的元模型建模”,是指“ 级模型的每一个元素都是级模型的恰好一个元素的实例”。 . 形式化语义的研究 语法结构虽然采用了形式化的规约,但其语义部分则是用自然语言描 述的,缺乏精确的形式化语义,这使得对模型难以进行定量定性的分析和验证。 针对这一问题,形式语义的研究已经成为国内外学术界关注的热点。对此 类问题研究的意义主要表现在以下几个方面: 清晰的解释。如果某一个组件在某一点上的意思存在混淆,形式化语义 可以作为参考来验证它的解释。 严格的分析与设计。如果与模型有关的概念用形式化描述技术去 表达, 那么将使得对图形执行严格的语义分析成为可能,从而可以对系统进行严格的评 估和实施。 等价性与一致性。它将为与其它技术和符号的对比提供一个不具有二义 性的基础,并且保证了内不同模型元素之间的一致性。 目前,学术界对语义进行形式化研究的两个主要思路是: .对核心语法进行形式化,使得成为符合形式化规范的语言。中山大学硕士学位论文 比较有代表性的是英国的作组 ”,这是一个由研 究人员和实践人员组成的国际性组织,其目标是运用浅显的数学知识将发 展成为一种精确形式化的建模语言。他们在元模型层次进行形式化,是一种 相对治本的办法,可保证在此基础上建立的模型层和用户对象层有可靠的 数学模型基础,为构造、操纵和细化模型提供一种通用的办法,但工作难 度较大。文献【】根据和谓词转换,提出一种面向对象的形式规范说明方法, 并给出一组和相对应的数学模型。文献【定义了一种包含对象流 描述 的活动图的形式语义,并根据语义,对活动图的典型流程以及活动图所描 述的动态系统的正确性进行了分析。文献【】对状态图中的各种状态以及变迁函 数进行了形式化定义,进而给出了状态机的组合操作语义。 利用形式化语言在不丢失或少丢失信息的前提下对进行形式化。该 方法对每一种图形赋予形式化语义,.然后就可以利用己有的形式化语言和 工具对模型进行推理验证。近几年大多数关于形式化语义的研究都 是基于这一思想的。 基于模型方法的转换 文献【】采用?语言规范对状态机视图进行了形式化描述,将 状态机中的各种状态模式转换为语言的模式运算来表达;文献【】采用语言 为的类图建立了形式化模型,并对类图的一些性质进行了分析和验证。 基于制动机的转换一 文献【】将状态图的操作映射到一个特定形式的自动机,使用基于自动 机理论的模型检验方法来验证 的线性时态逻辑性质;文献【】提 出了一种通过时间化自动机来形式化带有时问扩展的状态图的方法,这种 方法为与形式化方法的结合构造了桥梁作用。 基于网的转换 文献【】把用例图、对象图映射为时间网;文献【】提出了将活 动图转化为标记控制网的形式化方法;文献提出了一种特殊类 型的高级网与相结合;而文献【】将状态图转换为对象? 网,进而利用网的理论知识对所得到的网模型进行分析和验证。 基于验证工具语言的转换 中山大学硕士学位论文 文献【】对顺序图模型的自动验证方法进行了研究,在把顺序图转换 为模型检验器的输入语言后,使用模型检验器来验证系统设 计模型是否满足某些关键性质需求。 基于逻辑方法的转换 文献【】使用通用高阶逻辑形式规范语言来对进行形式化,给出 了状态图到规范的转换模型与规则。文献【 】采用实时动作逻辑&让 对的类图和状态图模型作形式化描述与精化,进而在此过程中进行验证。 . 模型的一致性 .. 模型一致性问题产生的原因 通过上面的分析可以看出,自身的不精确性会导致一致性问题的产生, 此外还有建模人员使用上的问题。我们将模型一致性问题产生的原因归纳 为以下几点: . .自身语义的不确定性 由于目标是成为一种面向对象的通用的建模语言,为了增加语言描述 的灵活性和通用性,并没有采取完全形式化描述,因此,对于同一种语义 需求,不同的人可能采取不同的表达方式,这些不同的表达之间可能存在一致性 问题。 .多视图间的信息冗余 的多视图机制可以降低系统设计的复杂性,但是这些视图并不是孤立 存在,而是彼此间相互关联,存在信息的冗余,这些冗余信息问也有存在不一致 的可能。 .违反标准、模式、规范等 对于标准、模式、规范等,在建模过程中,都是需要遵守的,这样可以提高 设计的质量和重用性。但是由于错误的理解或者使用,模型的表达可能与正确的 要求不一致。中山大学硕士学位论文 .. 模型一致性分类方案 的图形化、半形式化以及比较容易学习,使它成为目前的主流建模语 言。我们可以从两个层次认识一致性问题。第一个层次是从描述语言的角 度来看待一致性问题,因为是一种语言,因此它也满足通常语言的基本要 求。第二个层次是从对目标系统构建一个实际模型的角度看待一致性问题,此时 的不一致问题是在实现设计概念中产生的。 .根据模型的角度分类 从模型的角度考虑,一致性问题分为模型内部一致性和模型间一致性。 提供了用多视图来对单一系统建模,其范图从结构如类图、对象 图等 到行为如交互图、状态机图等。模型内部一致性包括视图内一致性和视图间 ~致性。视图内一致性是指同一视图内定义的元素满足形式化规则,有意义的连 接在一起。视图间一致性是指不同视图间定义的用来描述同一事物的元素能不冲 突的连接在一起。视图间一致性包括结构和行为两个方面。结构一致性需要检查 视图间的语法定义是否满足形式化规则,并且是静态一致的。行为一致性需要检 查不同视图内定义的同一需求是否满足语义一致性。一个支持多视图建模的语言 应该拥有一个共同的语义基础,来保证不同视图间的语义一致性,但是目前 还未实现这方面的需求。 模型问一致性是多个模型问的关系,这些模型通常是通过一系列的转化关系 彼此相联系。由于我们讨论的问题仅限于表示的模型,因此在这里,模型 问的一致性是指同一系统的不同版本的模型间的一致性问题。通常这种一致性问 题都是由于细化引起的,细化可以使一个模型从一个相对抽象的层次到一个更加 具体的层次。 .根据语言的角度分类 从语言的角度考虑,一致性问题可以被分为语法一致性和语义一致性两种。 语法是语言的表达方式,只关注于如何表达语言,不考虑其意思,语言的意思由 语义来表达。计算机工具只能处理语法,一种编程语言必须具有严格缤密的语法 结构,才能让计算机编译。但是没有语义的语法也是毫无意义的,计算机不可能 去猜测某个符号或文字的意思,语义的职责就是将无歧义的意思分配给语法,任 何可信赖的语义必须在两个方面保持一致性:语义领域和从语法到语义领域的映 中山大学硕士学位论文 射。语言的语法是通过其元模型来表示的。元模型是一个模式,它精 确定义了创建模型所需的构造物和规则。一个模型如果不能满足元模型,那么它 是不一致的。然而,即便满足元模型的模型仍有可能不一致,这主 要是由 元模型定义的元语言的表达能力造成的。为了对元语言进行补充,又给出 了,一个高阶逻辑语言,用来对的良构性做约束。是一个单纯 的表达语言,用来检查对象及其结构,并返回/值,但是它并不修改模 型。用表达的良构规则通常是进行更进一步的一致性检查所必须满足的前 提条件。下面是一些用表达的良构规则的例子: .任何元素都不能直接或间接的包含自己 .? .被拥有的元素必须有一个拥有者 . ? 与其他形式化语言不同,的很多语义是没有被精确的定义,这样就造 成多种解释的存在。例如,在多继承中,并没有明确规定如何继承同名属性。这 种不确定性是一把双刃剑,一方面,它使建模者在更高抽象层次上更加柔性的表 达设计,不用过早的考虑细节;另一方面,却因为缺乏精确和完整的语义说明使 得一致性检查更加困难。 .. 模型一致性检测方法 对软件设计中不一致性问题的研究,人们提出了多种处理方法,其中比较突 出的成果包括等提出的/。等提出了通过使用一阶逻 辑来验证模型的:和提出基于一致性管理的设计向 导方法。其他主要的成果还包括在需求分析中的一致性研究,尽管这些工作主要 集中在需求说明,但是其很多思想却和解决设计的一致性问题相类似。 目前,对于一致性检测的方法,我们可以将其归纳为四种类别:第一类是人 工审查技术。这类方法是以人工方式自顶向下对模型进行阅读,对模型中任何可 能导致信息不一致的因素进行评审。第二类,是试图完善元模型,前面提 到,缺少精确的语义,只是以非形式化的文字形式进行描述,因此该类研 究就是想通过定义更加完善的元模型来尽量减少非形式化的语义描述。第三类,中山大学硕士学位论文 是试图加强元模型中表达约束的语言。第四类,也是研究最广泛的一类, 形式化表示方法,将模型转换为一种更加形式化同时更便于分析的表达后, 再进行一致性分析。 .元模型方法 元模型方法试图对元模型定义一种完全形式化的语义,他们认为一个 更加形式化的可以更容易的进行一致性检测。他们将可以形式化的约束都 作为语法,只是将那些不能形式化的作为语义,例如“附加在衍型上的约束不能 与其所继承的衍型的约束相矛盾,也不能与其相关的基类的约束相