（计算机软件与理论专业论文）基于模型检测的uml形式化验证及其系统实现.pdf

中山大学硕士论文 基于模型检测的u m l 形式化验证及其系境实现 基于模型检测的u m l 形式化验证 及其系统实现 硕士生：朱泽涛 指导教师：张治国 计算机软件与理论 摘要 u m l 是面向对象开发中一种可视化建模语言，已经成为事实上的面向对象 建模标准。虽然表达丰富，但u m l 不是形式化的建模语言，其图形化的符号经 常缺乏精确的语义，这使得对u m l 进行形式化推理十分困难。为了保证系统设 计的正确性，在系统开发早期的时候发现可能存在的错误，进而降低系统开发的 风险，对u m l 模型进行形式化验证很有必要。 本文选取了u m l 模型的一个包括类图、状态图、顺序图或协作图的的子集， 研究了u m l 模型子集的n u s m v 形式化语义，定义了u m l 语义向n u s m v 语 义转换的一系列规则，使得可以对半形式化的u m l 模型进行n u s m v 形式化转 换，并在此基础上加以形式化验证，对于形式化验证，本文采用了模型检测的方 法。对n u s m v 形式化验证的结果，本文进行了分析，并且讨论了如何将之转换 为u m l 模型的逆向工程的方法，对此同样定义了将结果逆向工程到u m l 的一 系列规则，使得能够对u m l 的形式化验证结果逆向转换为u m l 模型。本文还 进一步设计并实现了基于上面转换规则的u m l 向n u s m v 语义转换以及从 n u s m v 逆向到u m l 模型的转换工具，并将这两个方向的转换以及n u s m v 模 型检测工具整合在一个系统中，实现了对u m l 的自动形式化验证。 我们在b o f l a n dt o g e t h e r 等环境中测试和验证本文定义的规则和实现的系统 的正确性，分别建立两个不同应用领域的u m l 模型，利用我们实现的系统对两 个实例进行n u s m v 转换，并对n u s m v 验证的结果逆向转换为u m l 模型，从 而实现了对于给定实例的自动化验证。实际的测试与验证说明了该系统能够运用 中山大学硕士论文 基于模型检测的u m l 形式化验证及其系统实现 于软件开发的过程及其基于u m l 的开发环境与工具中。 论文的成果，不仅在理论上讨论了对半形式化u m l 模型语义的形式化及其 逆向工程的一种可能性，而且在软件开发环境中实现了u m l 模型自动化验证的 实例系统，这对于实际的软件开发过程也具有很强的实用意义。 关键字：u m l ，语义转换，形式化验证，软件过程，模型检测 l j 生盔兰堡圭堡塞 茎主壁型丝型塑旦姓垄苎垡壁堡墨苎茎竺茎墨 af o r m a lv e r i f i c a t i o ns y s t e mf o ru m l m o d e l sb a s e d o nm o d e lc h e c k i n g s o f t w a r ea n dt h e o r e t i c a lc o m p u t e rs c i e n c e n a m e ：z h uz e t a o s u p e r v i s o r ：z h a u gz h i g u o a b s t r a c t u m li sav i s u a lm o d e l i n gl a n g u a g e i ti sb e c o m i n gad e f a c t os t a n d a r df o r o b j e c t - o r i e n t e dm o d e l i n g n e v e r t h e l e s s , i ns p i t eo fi t se x p r e s s i o nr i c h n e s s ，u m li s n o taf o r m a lm o d e l i n gl a n g u a g e t h eg m p h i c a ln o t a t i o n sa r co f t e nl a c ko fp r e c i s e s e m a n t i c s ，a n dt h i sr e d u c e st h ep o s s i b i l i t i e so ff o r m a lr e a s o n i n go nu m ld i a g r a m s i n o r d e rt og u a r a n t e et h ec o r l 优t n e s so f s y s t e md e s i g n , d e t e e tl a t e n te 墙i ne a r l yp h a s e a n dr e d u c et h er i s k so ns y s t e md e v e l o p m e n t , i ti sv e r yn e c e s s a r yt of o r m a l i z ea n d v e r i f yu m l m o d e l s t h i st h e s i sc h o o s e sas u b s e tf r o mu m lm o d e l s ，i n c l u d i n gc l a s sd i a g r a m s , s t a t e c h a r t s ，s e q u e n c ed i a g r a m so rc o l l a b o r a t i o n s ，r e s e a r c h e st h en u s m vf o r m a l s e n u m t i c so f t h es u b s e t ，w ed e f m eas e r i e so f t r a n s f o r mr u l e sf r o mu h 缸t on u s m v s e m a n t i c s ，w h i c hm a k e st h ef o r m a lv e r i f i c a t i o no fs e m i - f o r m a l i z e du m lp o s s i b l e m o d e lc h e c k i n gi su s e di nt h ef o r m a lv e i l f i c a t i o n t h et h e s i sa l s oa n a l y s e sa n d d i s c u s s e st h er e v e r s ee n g i n e e r i n gf r o mt h en u s m vv e r i f i c a t i o ni n f o r m a t i o nt ou m l m o d e l s w ea l s od e f i n eas e r i e so fr u l e sf o rt h er e v e r s ee n g i n e e r i n g ，w h i c hm a k e st h e v e r i f i c a t i o nr e s u l t sa g a i nt r a n s f o r m e di n t ou m lm o d e l s b a s e do nt h ea b o v e w o r k ，a s y s t e mw h i c hi n t e g r a t e st h et r a n s f o r m a t i o no f u m lt on u s m vs e m a n t i c s ，t h er e v e r s e e n g i n e e r i n gf r o mn u s m v t ou m lm o d e l sa n dn u s m vm o d e lc h e c k i n gi sd e s i g n e d a n di m p l e m e n t e d w ec a n 嘴t h es y s t e mt of o r m a l i z ea n dv e r i f yu m lm o d e l s a u t o m a t i c a l l y i nb o r l a n dt o g e t h e ra n do t h e re n v i r o n m e n t ，w et e s ta n d v e i l f yt h ec o r r e c t l l e s so f t h et r a n s f o r m a t i o nr u l e sa n dt h es y s t e mw ei m p l e m e n t t w ou m lm o d e l sf r o m d i f f e r e n td o m a i n sa r e 辩tu p ，t h e nt r a n s f o r m e di n t on u s m va n dt h er e s u l t so f n u s m v a r et r a n s f o r m e db a c kt ou m lm o d e l si no u r s y s t e m t h et e s t sa n dv e r i f i c a t i o n ss h o w i 中山大学硕士论文 基于模型检测的u m l 形式化验证及其系统实现 t h a tt h es y s t e mw o r k sw e l li ns o f t w a r ep r o c e s s e sa n d d e v e l o p i n ge n v i r o n m e n t sb a s e d o n u m l t h eo u t c o m e so ft h et h e s i sn o to n l yd i s c u s sap o s s i b l ew a yt of o r m a l i z et h e s e m i - f o r m a l i z e du m lm o d e ls e m a n t i c sa n di t sr e v e r s ee n g i n e e r i n gt h e o r e t i c a l l y , b u t a l s oi m p l e m e n ta na u t o m a t e du m lf o r m a lv e r i f i c a t i o ns y s t e mi na c t u a ls o t h a 1 e d e v e l o p i n ge n v i r o n m e n t ，w h i c hh a sas i g n i f i c a n tp r a c t i c a lm e a n i n gi ns o f t w a r e d e v e l o p i n gp r o c e s s e s k e yw o r d s ：u m l ，s e m a n t i ct r a n s f o r m a t i o n ，f o r m a lv e r i f i c a t i o n ，s o f t w a r ep r o c e s s ， m o d e lc h e c k i n g 中山大学硕士论文基于模型检涮的u m l 形式化验证及其系统实现 1 1 问题陈述 第1 章问题陈述与背景 统一建模语言( u n i f i e d m o d e l l a n g u a g e ) i l l 是面向对象开发中一种可视化建模 语言，在系统设计中已经获得了广泛的承认，并在多个领域中有成功的应用，已 经成为事实上的面向对象建模标准。u m l 通过捕捉系统静态结构和动态行为信 息来为系统建立各种模型，利用用例图、类图、状态图、顺序图、协作图等图形 符号来描述特定的系统，描述能力强大且表达直观，为软件开发人员提供了从系 统需求分析、设计到实现的有力支持。 2 1 但是，在随着u m l 的日益广泛应用，软件设计变得越来越庞大复杂，软件 系统的完整性和正确性很难被证明。u m l 虽然表达丰富，但u m l 不是形式化的 建模语言，其图形化的符号经常缺乏精确的语义，这使得对u m l 进行形式化推 理十分困难。例如，没有办法检验u m l 图是否满足给定的性质。当前，u m l 的 应用已经深入到各个领域，其中一些对系统的质量要求非常高，一旦出错将会造 成重大损失。为了保证系统设计的正确性，在更早的时候发现可能存在的错误， 进而降低软件开发的风险，对u m l 模型进行形式化并验证非常必要。 形式化方法在软件方面的应用原则上就是用数学与逻辑的方法描述和验证 软件，其目的是保证计算机软件的正确性。从验证来讲，主要有两类方法，一类 是以逻辑推理为基础，另一类则以穷尽搜索为基础。模型检测 3 1 属于后者，是一 种确保设计规范正确性的形式化自动验证技术，其实质是通过建立系统的有穷状 态模型，对这个模型的状态空间进行搜索，确定系统是否满足期望的属性。模型 检测在工业应用和协议分析中取得了巨大成功。 本文将基于模型检测技术，对u m l 模型进行形式化验证。本文的研究针对 u m l 模型的一个子集进行，并在u m l 各模型元素不存在逻辑冲突的假设上，分 别讨论每一种子集中的u m l 模型向形式化的n u s m v 语义转换的方法，并定义转 生哒掌硕士论文基于模型检测的u m l 形式化验证及其系统实现 换规则。对于n u s m v 形式化验证的结果，本文将进一步进行分析并讨论其逆向 工程到u m l 模型的规则。本文还将实现基于上面规则的从u m l 向n u s m v 语义转 换删n u s m v 反例逆向转换到u m l 模型的系统，实现u m l 的自动形式化验 证。 1 2 相关研究与技术 1 2 1 u m l 统一建模语言 u m l ( 统一建模语言) 是b 0 0 c h 等人1 9 9 5 年提出建模方法，用于对面向对 象系统可视化建模，是一种描述能力强大且表达直观的可视化建模语言，它通过 用例图、类图、协作图、状态图等一系列图形符号来描述特定的系统。支持不同 层次的系统抽象，能够清晰而准确地描述特定系统的结构、功能和行为，为软件 开发人员提供了从系统需求分析、设计到实现的有力支持。1 9 9 7 年o m g 将 u m l i 1 作为行业标准。由于u m l 图形丰富、完整的面向对象系统表现能力， 已经被许多软件公司用作软件系统建模工具。同时，出现了r a t i o n a lr o s e b o r l a n d t o g e t h e r ，m i c m s o rv i f i o 等可视化建模工具，加快了u m l 的广泛应用。目前 u m l 的最新版本是2 0 版。 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 是一种通用建模语言。对于一些专门 领域，例如用户图形界面( g u i ) 设计、超大规模集成电路( v l s i ) 设计、基于 规则的人工智能领域，使用专门的语言和工具可能会更适合些。u m l 是种离 散的建模语言，不适合对诸如工程和物理学领域中的连续系统建模。它是一个综 合的通用建模语言，适合对诸如由计算机软件、固件或数字逻辑构成的离散系统 建模。l i 】【2 】 1 2 2 形式化技术 随着软件的广泛应用，特别是软件在尖端领域的应用，软件可靠性成为一个 非常重要的问题。软件的可靠取决于两个方面，一个是软件产品的测试与验证， 另一个是软件开发的方法与过程。对简单的软件开发，我们的经验是先有对软件 的要求，然后对软件进行设计，然后是编写程序，最后是对程序进行测试，如果 测试出错则对软件进行修改，然后再测试直至对程序满意为止。对复杂的软件 系统，总的过程基本还是这样，只是各个阶段也相应复杂一些。比如说，软件的 要求可能需要从多方面进行描述，软件的设计需要从多方面考虑，程序的编写需 要分成多个单元，对于测试来讲也就有单元测试和总体测试的分别。有些软件的 要求难以一开始就完全清楚，而更改软件要求会对软件设计以及其他大量已经完 成或正在进行的工作产生很大的影响，因此有些软件开发方法和过程就需要提供 中山大学硕士论文基于模型检测的u m l 形式化验证及其系统实现 反复修改软件要求的便利。 【i i l l eln t m i l a r ) 图l l 软件开发过程中错误的引入、检测和耗费f 3 】 从上图的调查分析结果中可以看到，在软件开发过程中，错误的引入较多的 发生在系统设计和编程阶段，而错误被检测较多发生在系统测试阶段。然而随着 时间的推移，对错误的修正的成本在不断的升高。因而，对系统的验证，在软件 开发周期中的早期进行，可以很大的节省开发的成本。形式化方法的引入非常有 必要。 形式化方法在软件方面的应用原则上就是用数学与逻辑的方法描述和验证 软件。其目的是保证计算机软件的正确性。形式化方法的应用在电路设计和协议 设计上都取得了很大的成绩。对于软件来讲还有很多难以解决的问题。软件的描 述要比电路和协议复杂。软件系统的描述包括两个方面，即系统行为和系统性质。 因此研究的内容包括如何描述系统的这两个方面。从描述上讲，一方面是系统或 程序的描述，另一方面是性质的描述。这些可以用一种或多种语言来描述。这些 语言包括命题逻辑，一阶逻辑。高阶逻辑，代数，状态机，并发状态机，自动机， 计算树逻辑，线性时序逻辑，进程代数，开演算， 肛演算，特殊的程序语言， 以及程序语言的子集等。从验证来讲，主要有两类方法，一类是以逻辑推理为基 础，另一类则以穷尽搜索为基础。逻辑推理有n a t u r a ld e d u c t i o n , s e q u e n te a l c u l u s r e s o l u t i o n 以及h o a r e l o g i c 等方法。穷尽搜索方法统称为模型检测。这类方法与 4 中山大学硕士论文 基于模型检测的u 。形式化验证及其系统实现 系统或程序以及系统性质的表示有很大的关系，比如说符号模型检测，其基本原 理是用命题逻辑公式表示状态转换关系，用不动点算法计算状态的可达性以及这 些状态是否满足某些性质。从形式化方法的应用来讲，我们可以利用已有的方法 和工具，针对具体的问题进行分析，以保证软件的可靠性；我们也可以以目前常 见的软件开发方法为出发点，研究怎样将这些方法形式化，或研究怎样在软件开 发过程中增加一些形式化方法的应用，以提高软件的可靠性。【4 】 1 2 3m o d e lc h e c k i n g 模型检测技术 模型检测是一种确保设计规范正确性的形式化自动验证技术，其实质是通过 建立系统的有穷状态模型，对这个模型的状态空间进行搜索，确定系统是否满足 期望的属性。模型检测在工业应用和协议分析中取得了巨大成功。 图1 - 2 模型检测基本过程刚3 】 模型检测的基本过程可以从上图中表示出来。将现实中的系统进行建模，并 中山大学硕士论文基于模型检测的u m l 形式化验证及其系统实现 将系统的需求形式化为需求的描述，将它们输入到模型检测器中，如果模型满足 条件，则输h q y e s ，并对其他需求条件进行检验；如果条件不满足，则检测器会输 出反例，建模者就可以从中得到信息，对原来的模型进行修改后，再进行检验。 直到所有条件得到正确的验证，系统才满足了原先的需求。 模型检测的好处在于它有全自动化的检测过程，并且如果一个性质不满足， 它能给出这个性质不满足的理由。我们即可据此对我们的系统描述进行改进。模 型检测的困难首先是它所能检测的是有限状态模型。这样对于一般软件来讲，需 要有一个从任意状态到有限状态的建模过程。并且这样的一个模型的状态空间会 面临组合爆炸的问题。 目前m o d e lc h o c k i n g 的一些检验工具已经具有很强的功能，较常用的m o d e l c h o c k e r 包括：贝尔实验室开发的s p i n ，卡内基梅隆大学开发的s m v ，开放源码 的n u s m v ，美国国家航空航天局的j a v a p a t h f i n d e r ，以及j l i n t ，c o s p a n 等工具。 1 2 4 u m l 的模型检测技术研究 在u m l 的模型检测技术这一范畴上，近年来有着不少研究，国内外的研究 者们通过不同的角度和深度进行了探讨。 在国内的研究中，对u m l 类图的模型检测的研究，【4 】采用z 符号来表示u m l 类图的组成元素的语法和语义及其映射关系，最后对u m l 类图的一些性质进行 分析和验证；【5 】使用r a i s e 形式方法来表达u m l 类结构的含义；【6 】针对u m l 类 图和序列图的一致性问题，给出了判定类图和序列图一致性的必要条件和p v s 元理论，提出了一种基于定理证明器p v s 的一致性检验方法。 对u m l 状态图的模型检测的研究；阴用k r i p k e 结构定义s m 的操作语义，通 过检验从状态图翻译得到的i 【r i p k e 结构达到模型检测状态图的目的：【8 】把u m l 状态图中的状态映射到一种项代数上，再把状态项映射到种加标记的变迁系统 l t s 上，最后用操作语义s o s 规则归纳地给出满足组合性的u m l 状态机语义： 9 】 给出通过e h a 结构化她描述u m l 状态图及其语义的方法，然后用基于自动机理论 的模型检测方法验i 正u m l 状态图的l t l 性质；【l o 给出y u m l 状态图到p v s 规范 的转换模型与规则；【l l 】利用d f a 描述y u m l 状态图的语法，并采用z 语言对 6 中山太学弼i 士论文 基于模型检测的u m l 形式化验证及其系统宴现 u m l 状态图进行了形式化描述。 对u m l 顺序图的模型检测的研究，【1 2 】在把u m l 顺序图通过一系列规则转 换为p r o m e l a 语言后，使用模型检测器s p i n 来验证系统设计模型是否满足某些关 键性质器求； 1 3 】以序列图的事件序语义为基础，用消息序列表示序列图，并将其 具体上下文表示为对消息序列的语义约束，通过上下文约束与系统状态间的一致 性检查对序列图进行语义分析。 国内还有对u m l 可执行u m l 子集的模型检测的研究，f 1 4 】提出了一种用于 嵌入式系统u m l 模型验证的方法，采用与u m l 相同的符号表示法，并集成了状 态图所用的形式化语义定义。 在国内的这些研究中，基本都针对u m l 其中一种图例进行形式化研究，并 且基本都是提出方法，没有做出相关转换的工具。 在国外的研究中， 1 5 】利用了f u s i o n 建模技术和z 语言来描述u m l 模型， 【1 6 通过定义一系列规则将u m l 的一个实例转换为s m v 描述并进行验证，【1 7 】 对包括类图、状态图和活动图在内的u m l 模型自动转换为s m v 描述，对模型 的动态性质进行验证， 18 】中完成了一个u m l 验证工具，通过将u m l 转换为 s p i n 模型检测器识别的p r o m e l a 语言来对u m l 进行验证。并将检测信息转换为 u m l 顺序图，f 1 9 将u m l 转换为b 模型检测器所识别的形式化语言进行验证， 【2 0 基于抽象状态机使用了一个工具集来验证u m l 模型，【2 1 对现有的一些 u m l 模型检测技术进行了综述， 2 2 】完成了u s e 工具，对u m l 模型和o c l 约 束进行验证，【2 3 讨论了如何将u m l 模型转换为v i s 模型检测器识别的描述， 【2 4 同样将u m l 转换威s p i n 模型检测器识别的语言对u m l 进行验证，但方法 与【1 8 】有所不同，【2 5 】通过p v s 对类图、顺序图、活动图和用例图进行一致性检 验，【2 6 对u m l 的模型检测进行了综述，并提供了一系列将模型检测引入u m l 的规则，【2 7 针对一个工业控制系统的u m l 模型进行s m v 形式化的验证，【2 8 】 利用u s e t 具对u m l 模型和o c l 约束进行验证，【2 9 】展示了如何对协议的a g e n t u m l 进行验证，【3 0 对一个大型的航空冲撞防护系统的模型进行s m v 的形式化 验证，f 3 1 对一个生产零件进行u m l 建模并使用v u m l 工具对其进行验证。 对于u m l 状态图的模型检测的研究，【3 2 和【3 3 】利用s m v 模型检测器对 u m l 的状态图进行形式化验证，【3 4 】对u m l 状态图的s a f e t y 性质进行模型检测 并对其进行研究， 3 5 对u m l 状态图的语义进行形式化转换，其结果应用于 7 中山大学硕士论文 基于模型检测的u m l 形式化验证及其系统实璜 v u m l 工具上，【3 6 】对u i v i l 状态图形式化为冗算予，并利用n u s m v 模型检测 器对其进行检验。 对于u m l 状态图结合协作图的模型检测的研究，【3 7 1 和1 3 8 利用h u c k ) 对 u m l 状态图和协作图转换为p r o m e l a 语言并在s p i n 模型检测器上进行验证。 对于活动图的模型检测的研究，【3 9 】论述了一个对u m l 活动图所描述的工 作流图进行验证的工具t c m 。 对于u m l 可执行子集的模型检测的研究， 4 0 1 给出了一种通过将u m l 可 执行子集转换为c o s p a n 模型检测器识别的s r 语言并进行验证的方法。 在国外的这些研究中，u m l 图例基本都覆盖，各个文章所涉及侧重的u m l 图例有所不同，部分文章也完成7u m l 形式化的工具。 1 3 论文的主要工作 本文选取了u m l 模型的一个包括类图、状态图、顺序图或协作图的子集， 研究了u m l 模型子集的n u s m v 形式化语义，根据从非形式化到形式化的原则， 定义了一系列对各种u m l 语义向n u s m v 语义转换的规则。本文还进一步设计 了u m l 向n u s m v 转换的工具，通过u m l 向x m i 模型的转换，以及编写j a v a 程序来实现语义转换规则，来实现u m l 向n u s m v 转换的工具。 对于n u s m v 模型检测器得到的验证信息，本文进行了分析，并且探讨如何 将之逆向工程为u m l 模型表示出来，同样定义了一系列将结果逆向转换回u m l 的规则。本文也进一步设计了n u s m v 结果逆向转换为u m l 的工具，反过来通 过x m i 模型向u m l 模型的转换，以及编写j a v a 程序来实现反例转换的规则， 从而实现n u s m v 向u m l 逆向转换的工具。 本文还在上述两个工具的基础上，将它们和n u s m v 模型检测器进行整合， 从而实现了自动化验证u m l 的系统。 在本文的最后，还通过两个现实中的不同实例对论文的方法和系统进行实 验，从对实例进行u m l 建模，使用我们的系统对u m l 进行转换，得到的验证 信息，再将验证信息逆向转换为u m l 图，从而使得两个工具合并使用后的输入 和输出，都是u m l 的图例。 生生奎堂堡主丝苎 董王堡型丝型堕旦竺卫堕堑塑墅至翌苎墨! 1 2 哩 论文所设计并实现的系统，在整个u m l 形式化验证的过程中所起的作用， 在下面的图中表示出来： 图1 3 转换过程的总体设计图 整篇论文的主要贡献，在于它研究了u m l 的n u s m v 语义，并且定义了一 系列转换的规则，并且将u m l 形式化的验证整个过程设计并实现工具来完成； 不单如此，对于n u s m v 模型检测器的验证信息，本文还进一步分析了其逆向工 程为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 4 论文的结构安排 本文总共分为七章。 第1 章为问题陈述与背景部分，陈述问题，给出相关的研究与技术，指明论 文的主要工作以及论文结构。 第2 章到第6 章是本文的主要研究部分。 第2 章在理论上分析非形式化语言u m l 和形式化语言n u s m v 的语义，选 取一个包括类图、状态图、顺序图或协作图的u m l 子集，定义一系列规则使得 u m l 向n u s m v 语义转换。 第3 章是第2 章的实现。通过一个转换工具的设计和编码，实现第2 章的一 系列u m l 到n u s m v 的转换规则。 第4 章通过对待验证的性质的转换并验证后，分析n u s m v 的验证错误信息， 并定义规则将n u s m v 的反例转换为u m l 。 第5 章是第4 章的实现。通过另一个转换工具的设计和编码，实现第4 章的 一系列n u s m v 反例到u m l 的转换规则。 第6 章是第2 章到第5 章的应用实例，将两个不同应用领域的u m l 模型作 为输入，验证后将错误信息由u m l 输出。 第7 章总结全文并讨论进一步的工作。 中山大学硕士论文基予模型检测的u m l 形式化验证及其系统实现 第2 章u m l 的n u s m v 语义转换 2 1 非形式化语言u m l 的语义 在这一节中我们将对u m l 的模型所表达得语义进行分析。u m l 的概念和 模型可以分成以下几个概念域：静态结构、动态行为、实现构造、模型组织和扩 展机制。1 4 1 1 1 静态结构。任何一个精确的模型必须首先定义所涉及的范围，即确定有 关应用、内部特性及其相互关系的关键概念。u m l 的静态组件称为静态视图。 静态视图用类构造模型来表达应用，每个类由一组包含信息和实现行为的离散对 象组成。对象包含的信息被作为属性，它们执行的行为被作为操作。多个类通过 泛化处理可以具有一些共同的结构。子类在继承它们共同的父类的结构和行为的 基础上增加了新的结构和行为。对象与其他对象之间也具有运行时间连接，这种 对象与对象之间的关系被称为类问的关联。一些元素通过依赖关系组织在一起， 这些依赖关系包括在抽象级上进行模型转换、模板参数的捆绑、授予许可以及通 过一种元素使用另一种元素等。另一类关系包括用例和数据流的合并。静态视图 主要使用类图。静态视图可用于生成程序中用到的大多数数据结构声明。在u m l 视图中还要用到其他类型的元素，比如接口、数据类型、用例和信号等，这些元 素统称为类元，它们的行为很像在每种类元上具有一定限制的类。 在类图中类用矩形框来表示，它的属性和操作分别列在分格中。如不需要表 达详细信息时，分格可以省略。一个类可能出现在好几个图中。同一个类的属性 和操作只在种图中列出，在其他图中可省略。关系用类框之间的连线来表示， 不同的关系用连线上和连线端头处的修饰符来区别。 图2 l 是售票系统的类图，它只是售票系统领域模型的一部分。图中表示了 几个重要的类，如c u s t o m e r 、r e s e r v a t i o n 、t i c k e t 和p e r f o r m a n c e 。顾客可多次订 票，但每一次订票只能由一个顾客来执行。有两种订票方式：个人票或套票；前 中山大学硕士论文基于模型检测的u m l 形式化验证及其系统实现 者只是一张票，后者包括多张票。每一张票不是个人票就是套票中的一张，但是 不能又是个人票又是套票中的一张。每场演出都有多张票可供预定，每张票对应 一个唯一的座位号。每次演出用剧目名、日期和时间来标识。 图2 1 类图 类代表了被建模的应用领域中的离散概念物理实体( 如飞机) 、商业事物 ( 如一份订单) 、逻辑事物( 如广播计划) 、应用事物( 如取消键) 、计算机领域 的事物( 如哈希表) 或行为事物( 如一项任务) 。类是有着相同结构、行为和关 系的一组对象的描述符号。所用的属性与操作都被附在类或其他类元上。类是面 向对象系统组织结构的核心。 对象是具有身份、状态和可激发行为的离散实体。对象是用来构造实际运行 系统的个体；类是用来理解和描述众多个别对象的个别概念。 类定义了一组有着状态和行为的对象。属性和关联用来描述状态。属性通常 用没有身份的纯数据值表示，如数字和字符串。关联则用有身份的对象之间的关 系表示。个体行为由操作来描述，方法是操作的实现。对象的生命期由附加给类 中山大学硕士论文基于模型检测的u 池彤式化验证及其系统实现 的状态机来描述。类的表示法是一个矩形，由带有类名、属性和操作的分格框组 成。如图2 2 所示。 s u b e cr l p t i o n + s o r l e s ：s t r l n g * p r l c e c a t e g or y ：c a t e g o r y + a t b t b u t e l ：i n t e r g s r + c o s t ：m o n e y + o p e r a , o n l ： + c a n c e l l ： 图2 - 2 类表示法 用例视图是被称为参与者的外部用户所能观察到的系统功能的模型图。用例 是系统中的一个功能单元，可以被描述为参与者与系统之问的一次交互作用。用 例模型的用途是列出系统中的用例和参与者，并显示哪个参与者参与了哪个用例 的执行。 图2 - 3 是售票系统的用例图。参与者包括售票员、监督员和公用电话亭。公 用电话亭是另一个系统，它接受顾客的订票请求。在售票处的应用模型中，顾客 不是参与者，因为顾客不直接与售票处打交道。用例包括通过公用电话亭或售票 员购票，购预约票( 只能通过售票员) ，售票监督( 应监督员的要求) 。购票和预 约票包括一个共同的部分一即通过信用卡来付钱( 对售票系统的完整描述还要包 括其他一些用例，例如换票和验票等) 。用例也可以有不同的层次。用例可以用 其他更简单的用例进行说明。在交互视图中，用例作为交互图中一次协作来实现。 图2 - 3 用例图 b 凸口 2 动态行为。有两种方式对行为建模。一种是根据一个对象与外界发生关 系的生命历史；另一种是一系列相关对象之问当它们相互作用实现行为时的通信 方式。孤立对象的视图是状态机一当对象基于当前状态对事件产生反应执行作 为反应的一部分的动作，并从一种状态转换到另一种状态时的视图。状态机模型 用状态图来描述。 状态机视图是一个类对象所可能经历的所有历程的模型图。状态机由对象的 各个状态和连接这些状态的转换组成。每个状态对一个对象在其生命期中满足某 种条件的一个时问段建模。当一个事件发生时，它会触发状态间的转换，导致对 象从一种状态转化到另一新的状态。与转换相关的活动执行时，转换也同时发生。 状态机用状态图来表达。 图2 - 4 是票这一对象的状态图。初始状态是a v a i l a b l e 状态。在票开始对外 出售前，一部分票是给预约者预留的。当顾客预定票，被预定的票首先处于锁定 状态，此时顾客仍有是否确实要买这张票的选择权，故这张要票可能出售给顾客 也可能因为顾客不要这张票而解除锁定状态。如果超过了指定的期限顾客仍未做 出选择，此票被自动解除锁定状态。预约者也可以换其他演出的票，如果这样的 话，最初预约票也可以对外出售。 状态图可用于描述用户接口、设备控制器和其他具有反馈的子系统。它还可 用于描述在生命期中跨越多个不同性质阶段的被动对象的行为，在每一阶段该对 象都有自己特殊的行为。 中山大学硕士论文 基于模型检测的u m l 形式化验证及其系统实现 相互作用对象的系统视图是一种协作，一种与语境有关的对象视图和相互之 间的链，通过数据链对象间存在着消息流。视图点将数据结构、控制流和数据流 在一个视图中统一起来。协作和互操作用顺序图和协作图来描述。对所有行为视 图起指导作用的是一组用例，每一个用例描述了一个用例参与者或系统外部用户 可见的一个功能。 交互视图描述了执行系统功能的各个角色之间相互传递消息的顺序关系。类 元是对在系统内交互关系中起特定作用的一个对象的描述，这使它区别于同类的 其他对象。交互视图显示了跨越多个对象的系统控制流程。交互视图可用两种图 来表示：顺序图和协作图，它们各有不同的侧重点。 顺序图表示了对象之间传送消息的时间顺序。每一个类元角色用一条生命线 来表示一即用垂直线代表整个交互过程中对象的生命期。生命线之间的箭头连线 代表消息。顺序图可以用来进行一个场景说明一即一个事务的历史过程。顺序图 的一个用途是用来表示用例中的行为顺序。当执行一个用例行为时，顺序图中的 每条消息对应了一个类操作或状态机中引起转换的触发事件。 图2 - s 是描述购票这个用例的顺序图。顾客在公共电话亭与售票处通话触发 了这个用例的执行。顺序图中付款这个用例包括售票处与公用电话亭和信用卡服 务处的两个通信过程。这个顺序图用于系统开发初期，未包括完整的与用户之间 的接口信息。例如，座位是怎样排列的；对各类座位的详细说明都还没有确定。 尽管如此，交互过程中最基本的通信已经在这个用例的顺序图中表达出来了。 图2 5 顺序图 协作图对在一次交互中有意义的对象和对象间的链建模。对象和关系只有在 交互的才有意义。类元角色描述了一个对象，关联角色描述了协作关系中的一个 链。协作图用几何排列来表示交互作用中的各角色，如图2 - 6 。附在类元角色上 的箭头代表消息。消息的发生顺序用消息箭头处的编号来说明。协作图的一个用 途是表示一个类操作的实现。协作图可以说明类操作中用到的参数和局部变量以 及操作中的永久链。当实现一个行为时，消息编号对应了程序中嵌套调用结构和 信号传递过程。 图2 - 6 是开发过程后期订票交互的协作图。这个图表示了订票涉及的各个对 象间的交互关系。请求从公用电话亭发出，要求从所有的演出中查找某次演出的 资料。返回给t i c k e t s e l l e r 对象的指针曲代表了与某次演出资料的局部暂时链接， 这个链接在交互过程中保持，交互结束时丢弃。售票方准备了许多演出的票；顾 客在各种价位做一次选择，锁定所选座位，售票员将顾客的选择返回给公用电话 亭。当顾客在座位表中做出选择后，所选座位被声明，其余座位解锁。 顺序图和协作图都可以表示各对象间的交互关系，但它们的侧重点不同。顺 6 中山大学硕士论文基于模型检测的u m l 形式化验证及其系统实现 序图用消息的几何排列关系来表达消息的时间顺序，各角色之间的相关关系是隐 含的。协作图用备个角色的几何排列图形来表示角色之间的关系，并用消息来说 明这些关系。在实际中可以根据需要选用这两种图。 图2 - 6 协作图 u m l 还包括以下的概念域，但因为在论文中我们没有较深入的使用这些概 念域的u m l 图，所以在这里仅作概要的介绍。 3 实现构造。u m l 模型既可用于逻辑分析又可用于物理实现。某些组件代 表了实现。构件是系统中物理上的可替换的部分，它按照一组接口来设计并实现。 它可以方便地被一个具有同样规格说明的构件替换。节点是运行时间计算资源， 资源定义了一个位置。它包括构件和对象。部署图描述了在一个实际运行的系统 中节点上的资源配置和构件的排列以及构件包括的对象，并包括节点间内容的可 能迁移。 4 模型组织。计算机能够处理大型的单调的模型，但人力不行。对于一个 大型系统，建模信息必须被划分成连贯的部分，以便工作小组能够同时工作在不 同部分上。即使