（计算机软件与理论专业论文）基于动态逻辑的uml模型一致性检验.pdf

中山大学硕士学位论文 基于动态逻辑的u m l 模型一致性检验 基于动态逻辑的u m l 模型一致性检验 专业：计算机软件与理论 硕士生：郑炳喜 导师：周晓聪副教授 摘要 在基于u m l 的软件开发过程中，各种u m l 图形从不同侧面描绘着所开发 的软件系统，这些图形之间存在着信息的重叠，从而导致u m l 模型的一致性问 题。u m l 模型的一致性问题也是建模过程中一个重要并且需要解决的问题。 k e yt o o l 是一个支持形式化规范和代码验证的工具，该工具基于动态逻辑对 程序和形式化规范进行分析和验证，然而该工具并不支持在设计阶段对u m l 模 型进行一致性检验。作为k e yt o o l 的基础，动态逻辑不仅具备描述程序设计语 言的能力，而且能够描述u m l o c l 中的动态概念。因此，研究利用动态逻辑来 解决u m l 模型的一致性问题具有理论意义和应用价值。 本论文首先对u m l 模型存在的一致性问题进行综述，在此基础上深入分析 已有的方法，即骶g 提出的利用动态逻辑来检验u m l 模型一致性的方法中存 在的问题。g r e g 的方法只针对某一特定简单的u m l 模型进行设计，而本论文从 一般u m l 模型的基本要素出发来分析模型转换的方法，解决了原有方法中存在 的一些问题。并且，原有方法只支持类图、顺序图和状态图的检验，本论文对该 方法进行扩充，增加了o c l 规范与其他u m l 图形之间的一致性检验。 通过案例分析表明，改进和扩充后的方法不但能检验出更多u m l 图形之间 的一致性问题，而且能检验出0 c l 约束与其他u m l 图形之间的一致性问题。 关键词：u m l ，动态逻辑，一致性 m 中山大学硕士学位论文基于动态逻辑的眦模型一致性检验 u m lm o d e l sc o n s i s t e n c yc h e c k n gb a s e do nd y n a m i c l o g i c m a j o r ：c o m p u t e rs o 胁a r ea n dt 1 1 e o 巧 n 锄e ： b i n g x iz h e n g s u p e n r i s o r ： a s s o c i a t ep r o f e s s o rx i a o c h o n gz h o u a bs t r a c t i nt l l e p r o c e s so ft h eu m l - b a s e ds o r 、) r a r ed e v e l o p i n g ，a i r t i f i 虬t sr e p r e s e n t i n g d i 艉r e ma s p e c t so fm es y s t e ma r ep r o d u c e d t h eo v e r l a p p i n gi o 姗a t i o n 锄o n g t h e s e 狐i f a c t sm a yr e s u l ti nc o n s i s t e n c yp r o b l e m so ft h eu m lm o d e l s k e yt o o lp r o v i d e sf a c i l i t i e sf o rf o r n l a ls p e c i f ；i c a t i o na n dv e r i f i c a t i o no fs o u r c e c o d e ，b u ti td o e sn o ts u p p o r tc o n s i s t e n c yc h e c l ( i n gf o rd y n 甜1 1 i cu m ld i a g r a m s a s 也e b a s eo ft h ek e yt b o l ，d y n a n l i cl o g i ch a st h ea b i l i t yt oc o p e 丽t l lb o t hr e a l 、阳r l d p r o g r a m m i n gl a l l g u a g e sa i l dd y n 锄i cc o n c e p t so fu m l o c l t h e r e f o r e ，i ti sf e a s i b l e a j l dv a l 眦出l et od e a l 、忻t ht h ec o n s i s t e n c yp r o b l e mw i t hd y n a i l l i cl o g i c 1 1 1 i sm e s i sg i v e sa i lo v e n r i e wo ft 1 1 ec o n s i s t e n c yp r o b l e m so fu m lm o d e l sf i r s t ， a n dt h e ne x p l o r e sg r e g sm e t h o d ，w 1 1 i c hu s e sd y n 锄i cl o g i cf o ru m lm o d e l c o n s i s t e n c y g r e g sm e t h o do m yc o n s i d e r sap a n i c u l a rs i m p l eu m l m o d e la u l dh a s m a n yo t h e rd r a w b a c k s d i 肫r sf r o mg r e g s 印p r o a c h ，t h i st h e s i sp a ys p e c i a la t t e n t i o n t ot 1 1 ee s s e n t i a lf e a t u r e so fu m ld i a 铲锄sw h e nt m s l a t i n gu m ld i a 舒锄s ，a i l d s u p p o i r t sc h e c k 洫gc o n s i s t e n c yb e t 、v e e no c ls p e c i f i c a t i o na n du m ld i a g r i m l s t h ec o n s i s t e n c yc h e c k i n gp r o c e s si si l l u s t r a t e db yac a s es t u d y ，w 1 1 i c ha l s os h o w s t 1 1 a tt l l ei m p r o v e dm e 吐l o dc a i ld e t e c tm o r eh n d so fc o n s i s t e n c yp r o b l e m so f u m l o c lm o d e l s k e y w o r d s ：u m l ，d y n a m i cl o g i c ，c o n s i s t e n c y 中山大学硕士学位论文基于动态逻辑的u 近模型二致罹橙验 原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研究 工作所取得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人 或集体已经发表或撰写过的作品成果。对本文的研究作出重要贡献的个人和集 体，均已在文中以明确方式标明。本人完全意识到本声明的法律结果由本人承担。 学位论文作者签名：槭 日期：撕8 年 月g 日 中山大学硕士学位论文基于动态逻辑的u m l 模型一致性检验 学位论文使用授权声明 本人完全了解中山大学有关保留、使用学位论文的规定，即：学校有权 保留学位论文并向国家主管部门或其指定机构送交论文的电子版和纸质版， 有权将学位论文用于非赢利目的的少量复制并允许论文进入学校图书馆、院 系资料室被查阅，有权将学位论文的内容编入有关数据库进行检索，可以采 用复印、缩印或其他方法保存学位论文。 学位论文作者签名：留避磊 日期：抽譬年r 月8 日 i i 翩虢【司扎节 日期：2 工略年s 月g 日 中山大学硕士学位论文基于动态逻辑的u m l 模型一致性检验 1 1 研究背景及意义 第1 章绪论 目前，统建模语言( u m l ，u 1 1 i f i e dm o d e l i n gl a n g u a g e ) 已经成为软件工 业中为大型、复杂的系统进行建模的标准。在面向对象的软件开发过程中，使用 u 】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 模型的一致性问题，2 0 0 2 年、2 0 0 3 年以及2 0 0 4 年的u m l 年会 都召开了关于u m l 模型一致性问题的研讨会。2 0 0 2 年的研讨会的议题主要关于 中山大学硕士学位论文基于动态逻辑的u m l 模型一致性检验 u m l 模型一致性的定义以及检验方法，2 0 0 3 则关注于软件开发过程中一致性问 题的实例，而2 0 0 4 的研讨会则主要讨论了一致性问题与软件开发过程中的细化 关系之间的联系。 为了避免u m l 模型存在的一致性问题，并使其语义更加精确，许多文章建 议为模型增加约束或者一致性规则【2 ，3 ，4 ，5 ，6 1 ，这时候，一个模型是不一致的当且 仅当它不满足给定的约束或者一致性规则。同样也有许多文章利用形式化的方法 来解决u m l 模型的一致性问题【7 ，8 ，9 ，1 0 1 。应用这种方法时，一般先将模型转换为 形式语言( 如b 【1 0 1 、进程代数c s p 【8 1 、代数语言c a s l 【1 u 或者描述逻辑【9 1 ) ，如果 转换后的形式语言满足一定的性质，那么就说模型是一致的。由于形式化语言本 身的特点，这种方式一般应用于u m l 模型的一个子集。 另外还有许多与u m l 模型一致性问题相关的工作，如p r e c i s eu m l 团队致 力于为u m l 定义精确的语义。 研究如何形式化表示u m l 模型的还有k e y 工程，该工程由p e t e rs c h m i t t 和 b e m h a r db e c k e r t 领导，目前是德国科布伦茨大学( u m v e r s 时o f k o b l e n z ) 、卡尔 斯鲁厄大学( u 1 1 i v e r s 时o fk a r l s m l l e ) 和瑞典查尔姆斯理工大学( c h a l m e r s u 1 1 i v e r s 时o ft e c h n o l o g y ) 联合开展的一项科研工程。 k e yt o o l 是由k e y 工程开发的一个支持形式化方法的软件开发辅助工具， 该工具将面向对象软件开发过程中的设计、实现和形式化验证集成在一起。k e y t o o l 通过使用动态逻辑，验证程序是否满足u m l 类图和o c l 约束，该工具的 核心是一个一阶动态逻辑的理论证明器( t 1 1 e o r e mp r o v e r ) 。 k e y 工程旨在通过开发相应的辅助工具，帮助开发人员书写形式化规范( 如 o c l ) 、分析形式化规范，并进行形式化验证，从而实现将形式化的方法应用到 实际软件开发过程中。 k e yt o o l 的主要功能包括1 3 】： ( 1 ) 支持形式化规范( o c l 约束) 的创建。 ( 2 ) 对o c l 约束进行形式化的分析。 ( 3 ) 验证程序是否满足形式化规范。 除了k e y 工程之外，还有许多利用动态逻辑或其他模态逻辑来形式化u m l 模型并解决相关问题的研究工作。 2 中山大学硕士学位论文基于动态逻辑的u 。模型一致性检验 r o s s i 及其合作者采用时态逻辑( t e m p o r a ll o g i c ) 来形式化地描述u m l 状态图 【1 4 j 。时态逻辑是模态逻辑的一个分支，与动态逻辑有许多共同的特性。在他们 的工作中，引入了称为l n i n t e 的模态时态逻辑，将状态图中的状态表示为传递 的间隔表达式，操作形式化表示为非传递的间隔表达式，事件表示为节点或时间 表达式。 用时态逻辑来表示状态图的目的同样是为了将形式化的方法应用到软件开 发过程中，并且该文章指出，在将状态图描述为时态逻辑后，能发现其中存在的 冗余问题。 l c m 是基于动态逻辑的形式规范语言，w i e 血g a 和s a a l ( e 探讨了如何利用 l c m 来对s m a e r m e l l o r 方法中的模型进行形式化【1 5 】。他们的工作主要分析了如 何形式化s h l a e r - m e l l o r 方法中的信息模型( i 1 1 f o 册a t i o nm o d e l ) ，状态模型( s t a t e m o d e l ) ，进程模型( p r o c e s sm o d e l ) 以及通信模型( c o m m u i l i c a t i o nm o d e l ) 。在 将上述模型转换为形式语言l c m 后，通过分析能发现模型中存在的歧义和冗余 等问题，并且文章指出了如何消除这些问题。 1 3 本文的研究动机和研究思路 k e yt 0 0 1 的重点在于程序的形式化验证，而在系统代码实现之前，k e y 只支 持对类图和o c l 规范进行形式化分析( 包括一致性检验) ，并未支持对类图和 o c l 约束之外的u m l 图形，比如顺序图和状态图进行形式化分析和一致性检验。 另一方面，一致性问题作为建模过程中的一个重要的问题，如果能在系统实 现之前，对u i l 类图、状态图、顺序图和o c l 约束进行一致性检验，是一项 非常有意义的工作。 而k e y 工具是基于一阶动态逻辑的，因此，本论文对如何利用动态逻辑来 验证u m l 模型中的一致性问题进行研究。 对于如何利用动态逻辑来解决u m l 模型的一致性问题，g r e g 提出了解决的 思路和可行的方法【1 7 】，但是，骶g 的工作只能说明用动态逻辑来解决u m l 模型 一致性问题的可行性。g r e g 的方法是针对特定的例子设计的，并且不支持对0 c l 约束的检验，因此，该方法存在着许多问题和不足需要进一步研究，需要进行改 中山大学硕士学位论文 基于动态逻辑的l m l 模型一致性检验 进和扩充。 比如，g r e g 的方法中定义的一个对象可以向另一个对象发送消息的条件是： s p ，z 舭，? d ( x ，m ，少) 三( c ，鲫s ( x ) = e e ) v ( 办p 口d ( 幻如( x ) ) = j p ，z dm 幻少)( 1 1 ) 在上面的定义中，对象z 可以向对象少发送消息m 的条件是：对象x 是一个外部 实体( 外部实体不受限制) 或者对象x 需要向对象y 发送消息。 但是，这样的定义是不充分的。这个定义并没有考虑到u m l 模型一致性规 则中“消息必须与方法相关联”这一规则，即接收消息的对象所属的类中要有与 该消息相对应的操作，并且该操作对调用对象应该是可见的18 1 。如下面的u m l 模型： 图1 1 顺序图 b 拌x ：s t r i n g 拌y ：s t r i n g + m e t h o d 2 0 + m e t h o d 3 0 图1 2 类图 在图1 1 中，类a 的实例( 对象) a 向类b 的实例( 对象) b 发送消息m e t h o d l ， 但是在类b 的定义中，并没有处理消息m e t h o d l 对应的方法。仅管这样，根据 g r e g 的定义，发送消息的条件依然成立。由此可见，s p 胛d 硝( x ，m ，少) 的定义 4 中山大学硕士学位论文基于动态逻辑的u m l 模型一致性检验 无法检测出该一致性问题。 此外，g r e g 的方法中也存在一些不适合一般u m l 模型的定义，如关于对象 接受一个消息的定义： x n c c e p t 暑 ! 蔓亟夏至暨觋三陋主里受蓟薹 f d ( 如( x ) ：= e ”f ，? 垆r d c ( s f 日f p ( x ) ) ； 砌( x ) ：= 幻玎( f ，z r 7 c 砂( x ) )( 1 - 2 ) 在上面的定义中，s 幻胞 ) ：= 刀耽s 砌陀( s 幻纪( x ) ，矗p d ( 砌f r 缈( x ) ) ) 表明一个对象接受 一个消息后，该对象马上进入由状态图中规定的一个新的状态，这样的定义与一 般状态的概念是不相符的。如图1 3 和图1 4 所示的模型： t 啪。行； o f r ： 一1 图1 3 顺序图 t u m o f r 【l a m p s t a t u s = o 御 o n。行 图1 4 类c o n t r o l l e r 的状态图 在图1 3 的顺序图中，对象c 接受消息t u n l o f r ，按照a c c e p t 的定义，c 进入 。厅状态，但是在图1 - 4 所示的状态图中，需要在l 锄p s t a t u s = o 仃成立后，才进入 o f r 状态，即需要等c 发送消息。行给对象l 锄p 并等待返回值后才进入新的状态。 上面x 口c c 印r 的定义完全忽略了对象在接收到消息后与其他对象的交互过程。 假如顺序图中消息o f r 被错误地写成o n ，对象c 获得的返回值是o n 而不是 中山大学硕士学位论文基于动态逻辑的u m l 模型一致性检验 o m 使得l 锄p s t a n j s = o n ，那么c 就不可能进入o f f 状态，但是x 口c c 印f 的定义仍 然使得c 进入。行状态。 对于这个问题，在第4 章中本文将通过定义一个新的程序x 如玎p ，通过x 如刀口 进行状态变迁，从而解决这一问题。 对于一般的u m l 模型来说，状态是某个情形的抽象，在该情形下，一定的 变量值维持不变，比如一个对象在等待外部事件或者执行完某操作后的静止的情 形。 g r e g 的方法存在不足的主要原因是他的方法只是从某一简单的模型出发去 设计。因此，为了解决已有方法存在的问题，需要进一步考虑适合于描述一般 u m l 模型中对象之间动态交互行为的定义，在进行u m l 图形转换时，需要从 图形的基本要素出发去考虑模型的转换。并且，扩充支持o c l 约束的检测，需 要分析o c l 约束与对象动态行为和对象状态变迁之间的关系。 1 4 本文的主要工作 本文的主要工作包括： ( 1 ) 对u m l 模型一致性问题进行概述，总结了u m l 模型一些典型的一致 性规则。 ( 2 ) 对已有的利用动态逻辑检验一致性问题的方法中存在的一些问题进行 改进。 ( 3 ) 对方法进行扩充，支持检验o c l 约束与类图、状态图和顺序图之间的 一致性。 ( 4 ) 将改进和扩充后的方法应用于一个典型的具体实例进行一致性检验。 1 5 论文的组织 本文第1 章是绪论，先介绍了u m l 模型一致性问题的研究背景、研究意义， 6 中山大学硕士学位论文基于动态逻辑的u i 咀。模型一致性检验 以及国内外的研究现状，接着说明了为什么选择动态逻辑来解决u m l 模型的一 致性问题，重点阐述了本文的研究动机，指出了已有方法存在的一些不足，最后 说明了本文的主要工作。 第2 章介绍了动态逻辑的相关基础知识。因为动态逻辑是模态逻辑的一个分 支，因此，第二章在介绍了模态逻辑一些相关概念的基础上，再引入动态逻辑。 第3 章对u m l 模型的一致性问题进行综述，介绍了u m l 模型一致性问题 的分类及其产生的原因，以及两种解决u m l 模型一致性问题的途径。 第4 章首先分析了u m l 模型的消息机制，以及如何利用动态逻辑中的程序 来定义对象之间的动态交互行为。接着，讨论了如何将u m l 模型的类图、o c l 约束、状态图和顺序图转换为动态逻辑公式。 第5 章引入了一个具体实例：m o n d e xe l e c t r o m cp u r s e ，并将该实例的模型( 类 图、o c l 约束、状态图和顺序图) 转换为动态逻辑公式。 第6 章则利用改进和扩展后的方法对第5 章引入的实例模型进行一致性检 验。 最后是总结与展望。 中山大学硕士学位论文 基于动态逻辑的u f v f i 。模型一致性检验 第2 章动态逻辑简介 动态逻辑是关于程序推理的形式系统。动态逻辑可以视为一阶谓词逻辑、模 态逻辑和正则事件代数( a l g e b r ao f r e g u l a re v e n t s ) 三者的结合【1 9 1 。动态逻辑区别 于经典逻辑的一个显著特点是它的动态性，在经典谓词逻辑中，真值是静态的， 而动态逻辑拥有程序的概念，可以通过程序改变变量的值，从而改变公式的真值。 动态逻辑是模态逻辑的一个分支，并且动态逻辑的语义也来源于模态逻辑， 因此，本章首先介绍模态逻辑的基本思想，然后再引入动态逻辑。 2 1 模态逻辑简介 模态逻辑是关于必然性和可能性的逻辑，也可以说，是关于“一定是 和“可 能是”的逻辑。 模态是指事物或命题的必然性和可能性等这类性质。模态逻辑在经典逻辑的 基础上，增加了新的连接词，表达模态的概念： 口( b o x )读作“是必然的 ( d i 锄o n d )读作“是可能的” 连接词口和称为必然算子和可能算子。 模态逻辑有多种语义学，其中最主要的一种语义学是可能世界语义学。可能 世界语义学来源于莱布尼茨关于必然性和可能性的观点：一个命题是必然的，当 且仅当它不仅在现实世界中为真，而且在所有可能世界中都为真。 在可能世界语义学的基础上，可以更加精确地定义可能性和必然性： 模态命题口p 在可能世界w 被认为是真的，当且仅当在与w 相关的所有可能 世界中，命题p 都是成立的。 模态命题p 在可能世界w 被认为是真的，当且仅当至少存在一个与w 相 中山大学硕士学位论文 基于动态逻辑的l m l 模型一致性检验 关联的可能世界w 7 ，在w 7 中，命题p 成立。 模态逻辑在计算机科学中有着广泛的应用。以模态逻辑为基础，可以建立多 种应用逻辑，如动态逻辑( d y 彻m i cl o g i c ) 、时态逻辑( t e n l p o r a ll o g i c ) 、表述逻 辑( d e s c r i p t i o nl o g i c ) 等等。 2 2 动态逻辑简介 动态逻辑是模态逻辑的一个分支，动态逻辑是一个关于程序推理的形式化系 统。传统上，动态逻辑可以用来形式化表示系统的规范以及证明程序满足这些规 范。动态逻辑也可以视为阶谓词逻辑、模态逻辑和正则事件代数三者的结合 【1 9 】 o 动态逻辑最显著的特点，是拥有一个称为“程序”的语法结构，它的主要作 用是改变变量的值，进而改变整个公式的值。例如程序“x ：= x + 1 ”改变了公式“x 是偶数”的真值【1 9 】。 动态逻辑通过一个模态结构 妒来讨论一个程序a 的执行对公式9 真值 的影响。这个结构直观的意思是：从当前状态开始执行程序a ，执行后停止在满 足公式妒的状态是可能的。 与该模态结构对偶的结构是 a ，它的直观意思是：如果a 从当前状态开始 执行并停止，那么它执行后所处的状态必定满足公式。 2 2 1 程序和命题 动态逻辑区别于经典逻辑最大的特点是它拥有程序的概念。给定一个原子程 序和测试的集合，正则程序可以按照下面的规则进行归纳定义： 任何一个原子程序或者测试是一个程序； 如果a 和卢是程序，那么口；卢是程序； 如果a 和卢是程序，那么au 卢是程序； 9 中山大学硕士学位论文基于动态逻辑的u m l 模型一致性检验 如果口是程序，那么a 是程序； 在命题动态逻辑中，原子程序是抽象的二元关系，而在一阶动态逻辑中，原 子程序是简单赋值语句x ：= f 。对于测试的概念，如果妒是一个公式，那么9 7 就 是一个测试。上面正则程序定义中使用的程序算子及其意义如下： ( 1 ) 程序算子： ；合成 u 选择 木 迭代( 重复) ( 2 ) 程序算子意义： a ；卢表示：执行程序a ，然后再执行程序卢。 au 卢表示：非确定地选择程序a 或者程序卢，然后执行它。 a + 表示：非确定地执行程序a 零次或者多次。 在动态逻辑中，通过使用混合算子，程序和命题可以进行相互定义： ( 1 ) 混合算子： 口 必然 ? 测试 ( 2 ) 混合算子意义： k 坳这是一个命题，表示：执行完程序a 后，命题妒必然成立。 9 7这是一个程序，表示：测试命题妒，如果9 为真则继续，否 则失败。 因此，动态逻辑中正则程序的定义应增加下面的规则： 如果9 是一个公式，那么妒? 是一个程序； 公式的定义也应增加规则： 如果9 是一个公式，a 是一个程序，那么【a 砂是一个公式； 1 0 中山大学硕士学位论文基于动态逻辑的in m ，模型一致性检验 2 2 2 一阶动态逻辑( d l ) 一阶动态逻辑在动态逻辑中的地位就像一阶谓词逻辑在经典逻辑中的地位。 在后面进行模型转换的时候，采用的是一阶动态逻辑，因此下面分别介绍一阶动 态逻辑的语法和语义。下文中，d l 【1 9 】表示一阶动态逻辑。 2 2 2 1 基本语法 在一阶动态逻辑中，有一个一阶词汇表，该词汇表包括了函数符号和谓词 ( 关系) 符号。基于该词汇表，可以定义程序集合和公式集合。并且，通过模态 算子 】和测试算子? ，程序和公式可以相互定义。 在d l 中，原子公式的形式是r ( ，乙) ，其中，是词汇表上的一个玎元的 关系符号，乙是上的项。 原子程序是简单赋值语句x ：= f ，其中z 属于变量集合矿，f 是词汇表上的 项，该赋值语句表示将项f 的值赋给变量x 。 在命题模态逻辑中，通过使用测试算子? ，可以把公式转换为程序，而在一 阶动态逻辑中，测试算子只能用于不包含量词的公式。 2 2 2 2 语义 d l 的语义来源于模态逻辑的语义，通过定义一个一阶结构( f i r s t o r d e r s t m c 眦) 来解释d l 中的程序和公式【1 9 1 。 定义一个词汇表上的一阶结构a ，a 是一个二元组a = ( 彳，) ，称为计算 域( d o m a j no f c o m p u t a t i o n ) 。在二元组似，) 中，彳是一个集合，称为一阶结构 a 的载体( c 删e r ) ，聊a 是一个意义函数( m e a i l i n g 劬c t i o n ) ，对于词汇表上 的n 元函数符号厂，解释为聊a ( 厂) ：彳”一彳，对于词汇表上的谓词( 关系) 符 号，解释为聊a ( ，) 彳”。 对于每个程序a ，都关联一个二元关系：聊a ) s a s a ，表示程序的输入 状态输出状态。赋值语句f ( ，乙) ：= f 解释为： 中山大学硕士学位论文基于动态逻辑的眦模型一致性检验 聊a ( f ( ，乙) ：= ，) 三 ( “，” f “( f ) “( ) ，“( f 。) “( ，) 】 ) l 甜s a ) 在d l 中，程序可以视为状态之间的桥梁，程序通过赋值语句改变变量的值， 而状态是对各个属性值的瞬间描述( s n a p s h o t ) 。在一阶谓词逻辑中，状态其实是 对变量集合的赋值( v a l u a t i o n ) 。从某一个输入状态开始，程序执行过程中经历 的状态序列称为迹( t r a c e ) 。 对于d l 中的每个公式妒，都关联着一个集合：( 妒) 冬s a 。d l 中公式的 语义定义为： ( o ) 兰g 聊a ( 9 寸l f ，) 兰 甜ii f “聊a ( 妒) t h e n “脚a 缈) ) ，竹a ( b k ，缈) 三 z ，iv 口a ，“ x 口】，竹a ( 9 ) ) 聊a ( 【a 】妒) 三以lv v ，i 坟u ，v ) 聊a ( a ) t h e n1 ，朋a ( a ) 2 2 2 3 可满足性和有效性 假设a = ( 彳，) 是一阶结构，甜是s a 中的状态。对于公式9 ，如果甜研a ( 9 ) ， 那么有a ，“| ：9 ，即满足9 。如果a 中任何一个状态“都满足9 ，那么称妒在a 中有效。 对于任何一个程序口从状态“开始的可终止的执行，在终止状态里都有妒成 立，那么就有a ，扰l = 【a 缈。 如果存在一个程序口从状态甜开始的可终止的执行，并且终止状态满足缈， 那么就有a ，甜l = 妒。 2 3 本章小结 动态逻辑是模态逻辑的一个分支。本章首先从模态逻辑开始，介绍了模态逻 辑的相关概念、基本思想及可能世界语义。接着，本章介绍了动态逻辑中程序的 1 2 中生盔兰堡主兰垡笙奎 茔王垫查望笙塑竺坠堡型二塾堡垒垦 - _ _ _ - _ _ _ _ _ _ - - _ _ _ - _ - - _ _ i _ _ _ _ - - - _ _ _ - _ - - - - _ _ _ _ _ _ _ - _ _ _ _ _ - 一一 概念以及动态逻辑公式的基本构造，然后介绍了一阶动态逻辑( d l ) 的语法和 语义。 本章的参考文献是 1 9 ，2 0 ，2 1 ，2 2 ，2 3 ，2 4 ，2 5 ，2 6 ，2 7 ，2 8 】。 1 3 中山大学硕士学位论文 基于动态逻辑的l m l 模型一致性检验 第3 章u m l 模型的一致性问题 3 1 一致性问题的分类及其产生的原因 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 表达式( 即模型元素的集合) 可以有多种解释，而其中某些解释可能 是不一致的【2 9 】。 本文讨论的一致性问题指的是水平一致性问题。 1 4 中山大学硕士学位论文基于动态逻辑的u m l 模型一致性检验 3 2 一致性问题的解决途径 3 2 1 基于规则( 约束) 的解决途径 为了尽量避免u m l 模型中存在的一致性问题，许多文章建议为模型增加约 束【3 ，5 ，6 ，1 8 ，3 0 ，3 1 ，3 2 1 ，以使模型的语义变得精确。增加的约束可以使用o c l 或者其 他方式来表达。在这种情况下，一致性的定义是：一个模型是一致的当且仅当模 型遵循增加的约束。 这种基于规则( 约束) 的方法首先要定义一致性规则，然后通过硬编码的方 法将规则嵌入到工具的实现中。利用这种方法，可以在模型创建过程中，对可能 导致模型不一致的行为实时地进行检查和预防【1 8 】。 典型的一致性规则可以总结如下【3 ，5 ，3 0 ，3 3 】： ( 1 ) 类图和交互图之间的一致性规则： 规则1 如果两个对象之间有消息传递，则这两个对象所属的类之间应该要 有关联关系。 规则2 接收消息的对象所属的类中应有与该消息相对应的操作。 规则3 交互图中消息的参数类型和次序，应与类图中定义的参数类型和次序 一致。 ( 2 ) 类图和状态图之间的一致性规则： 规则1 类被删除时，其状态图要一同被删除。 规则2 状态图中的每一个触发事件，在类图中必须有相应的操作与之对应。 规则3 状态图中的每一个动作，必须在状态图所属的类的类图中进行定义， 动作的参数类型和次序必须与定义时的参数类型和次序一致。 规则4 用于定义状态的变量必须是相对应的类图中类的属性。 ( 3 ) 交互图和状态图之间的一致性规则： 规则1 某个类的状态图中每一个状态转移，都应能由交互图中该类的实例 所接收或发送的消息完成。 规则2 状态图中的每一个动作，必须对应到顺序图中相应对象的一个往外 发送的消息。 中山大学硕上学位论文基于动态逻辑的u m l 模型一致性检验 3 2 2 基于模型转换的解决途径 第二种解决u m l 模型一致性问题的途径是将模型转化为形式语言。这时候， 模型一致性的定义是：如果转换后的形式语言满足一定的性质，那么就说该模型 是一致的。 如h r a s c h 和h w 色r h e i m 提出了将类图和状态图转换为进程代数c s p ( c o m m u n i c a t i o ns e q u e n t i a lp r o c e s s ，通信顺序进程) ，并在一个共同的语义域里 给出一致性的定义方法【8 】o 如图3 1 所示： i 类图 l 将耋 1 p r o c z ， 图和状态图转化为 状态图 ；s p r p r o c 溯 0 口c r 如p ( x ) = 弦居p ( 4 4 ) 如表4 2 所描述，接收列表非空表明有其他对象向对象x 发送消息， 删略d “儿衙为空以及口c f f 馏为知垃表明x 并没有处于活动箱中，因此x 可以接受 消息聊曙0 ，执行该消息对应的操作。 中山大学硕士学位论文基于动态逻辑的明儿模型一致性检验 表4 2 辅助变量表 m s g r c v n s tm s g o m s g o m l l i s t o n c l i v e 矗l s e ( 2 ) 发送消息的条件： s p 胛d c d ，2 d ( x ，聊芦g ，y ) 皇 乃p 耐( ，船曙d “圮括，( x ) ) = s p 咒d ，挖号g ，d y 口c 疗坦( x ) = 驴“p ( 4 5 ) 捃r p 肠胞d ( c ，现路( x ) ，c ，a 镕( y ) ) 西功( ，扎蹭? ，c z 如( j ，) ) 其中，括r e 肠纪d ( c 琊( x ) ，c 厶琊( y ) ) 和括g p ( 聊曙，c 厶她，( 少) ) 是谓词，分别表示对 象x 和对象y 所属的两个类是否关联，对象y 所属的类是否有历蹭对应的方法。 表4 3 描述了对象可以发送消息时各个成员变量的情况，消息发送链表非空， 日c f f w 值为t r u e 。 表4 3 辅助变量表 m s g r c v n s t聊曙0 m s g o t l 也i s t s e n dm s gt 0y 口c f i v e 驴甜p ( 3 ) 操作可以完成的条件： 如刀竺焉等二“p 八j 妇( m 路。甜圮研( 纠：。 j 咖( 聊置非c 儿衙( 砌 。( 4 6 )口c ，如p ( x ) = 护“p 八j f 嬲( m s g d 甜圮西f ( x ) ) = o j z 砧( 聊蹭氓c v 厶函r ( x ) ) 0 、7 如表4 4 所描述，消息接收列表非空、消息发送列表为空并且口c f 眈的值为 肛“p 表明对象完成与其他对象的交互过程( 单个活动箱中) ，即可以完成消息 聊昭0 引起的操作。 中山大学硕士学位论文基于动态逻辑的埘l 模型一致性检验 表4 4 辅助变量表 m s g r c v n s tm 路0 m s g o “t l s t f 2 j 口c f f v p 驴甜p 下面以个对象对一个消息的处理过程为例，说明在处理过程中各个引入的 辅助变量的值的变化。 “o o t ，一 m s g l 。 ( x s p ，z d ，”陷，z m s 9 2 。 b 。s e n dm s g ：l ，y h 口、 m s g r c v n s tm s g o m s g o l l t l i s t g n c t 如e 砖l s e s t q t e s o m s g r c 、 n s t m s g o t l f l i s t m s g o s e n dm s g jt oy s e n dm s 9 2t oz n c t i v et r u e s l a t e s o 力 m s g r c v l i s t 肌曙d “圮衙 8 c t i v e s t n t e m s g o s e n dm s 9 2t oy 打秘e z m s g r e v n s tm s g o m s g o u t n s t 仍 8 c t i v e协t l e s t n t e s o m s g r 铡n s t m s g o u f l i s t a c t i v e s t q t e 图4 2 辅助变量变化示意图 在图4 2 中，当外部对象向对象工发送消息聊唧时，肌曙d 被放到x 的消息接 收列表m 啦c 儿纽中去，表明已经有消息发送给x 。此时口c c 印f c 6 以( x ，肌蹭d ) 成 p 彩彩伽墨 中山大学硕士学位论文 基于动态逻辑的u m l 模型一致性检验 立，执行x 口c c 印f ，把x s p 刀d 优路，d y 和z s 绷d 朋呼幻z 放到垅曙d “圮括，链表中， 口c f f w 的值变为驴“p 。这时候，s p 刀次为，? 讹聊曙j ，成立，执行程序 x s e 扎dm s g 】l oy ，龄s e n d c o n d ( x ，m s 9 2 y ) 矗屯立，萄沁i 程序x s e n dm s 9 2t ozo 最 后，执行x 如门p ，口c ，f w 的值改为如船，对象进入新的状态_ 。 下面分析u m l 中状态与d l 中状态的对应关系，如图4 3 。 u m l 状态d l 状态 图4 3 模型中状态和d l 中状态对比示意图 在d l 中，程序是状态之间的桥梁，对应每个程序，都有一个输入状态和输 出状态。而在u m l 视图中，当完成消息对应的方法时，才变迁到一个新的状态。 因此，在x 如门p 中，才对对象的状态值s 砌胞做出修改。而在执行x 口c c 印，和x 肥力d 时，并不需要修改变量s 砌纪。 2 4 中山大学硕士学位论文基于动态逻辑的u m l 模型一致性检验 通过定义三个程序以及它们执行的条件，可以得到描述系统可能发生的行为 的程序： 删d ，z 暑( ( s p 玎胁刀讹嘴，y ) ? ；艘，z dm 路幻y ) u ( 4 7 1 ( 口c c 够p f c d 玎d ( x ) ? ；x 口c c 9 p f ) u ( c 幻刀p c d ，2 d ( z ) ? ；x ( 幻疗p ) ) 木 、7 其中，表示程序可以执行o 次或者多次。 4 2 确定d l 的基调 在u m l 模型中，通过发送带参数或不带参数的消息调用对象的方法，并且 一般从方法的返回值获取结果。在逻辑中，相对应的概念是函数和谓词，函数根 据它的参数得到一个值，而谓词的值为真或者为假，换句话说，一个谓词可以视 为是一个布尔值函数。在逻辑中，一般将函数和谓词分开表述。 4 2 1 类型和基调 在逻辑中，对谓词和函数的参数类型和返回值类型的一系列声明，称为基调 ( s i g n a t u r e ) 【3 6 1 。 在定义基调之前，先将u m l o c l 中的词汇映射到d l 中的词汇【1 2 】，如表4 5 所示： 表4 5 词汇映射表 u m l o c ld l 类同名的一个类型 基本类型( m t e g e r ，r e a l ，b o o i e a i l ， 相应的抽象数据类型 s t r i n g ，) 0 c l 集合类型【3 7 1 s e t t ，c o l l e c t i o ，s e q u e n c e t ，b n g t 其中，t 表示类型，并记类型的集合为t 。 接着，定义在该类型集合t 上的一个基调为四元组s m ，f s y h l ，p s m ，a ) 3 6 】， 中山大学硕士学位论文 基于动态逻辑的u m l 模型一致性检验 其中： v s y m 是变量符号的集合； f s y m 是函数符号的集合； p s y i l l