2010 届研究生硕 位论文
学校 ：10269 学 号：51081201022
院 专
系：信息学院 机科学技术系 业： 机软件与理论 软件形式化验证 杨宗源 教授 谭 力
研 究 方 向： 指 导 教 师： 硕 研究生：
2010 年 4 月 完成
Thesis of Master's degree in 2010
School Code: 10269 NO.: 51081201022
Department: Major: Research Interest: Advisor: Master Candidate:
Computer Science and Technology Computer Software and Theory Software Formal Verification Professor Zongyuan Yang Li Tan
Fulfilled in April, 2010
华东师范大学学位论文原创性
郑重声明：本人呈交的学位论文《基于情态演算的 UML 形式化验证与 OCL 约束自动生成研究》 ，是在华东师范大学攻读硕士/博 请勾选）学位期间，在 导师的指导下进行的研究工作及取得的研究成果。除文中已经注明引用的内容 外，本论文不包含其他个人已经发表或撰写过的研究成果。对本文的研究做出重 要贡献的个人和集体，均已在文中作了明确说明并表示谢意。
作者签名：
日期：
年
月
日
华东师范大学学位论文著作权使用
《基于情态演算的 UML 形式化验证与 OCL 约束自动生成研究》系本人在 华东师范大学攻读学位期间在导师指导下完成的硕士/博 请勾选）学位论文， 本论文的研究成果归华东师范大学所有。 本人同意华东师范大学根据相关规定保 留和使用此学位论文， 并向主管部门和相关机构如国家图书馆、 中信所和 “知网” 送交学位论文的印刷版和电子版； 允许学位论文进入华东师范大学图书馆及数据 库被查阅、借阅；同意学校将学位论文加入全国博 硕士学位论文共建单位数 据库进行检索，将学位论文的标题和摘要汇编出版，采用影印、缩印或者其它方 式合理复制学位论文。 本学位论文属于（请勾选） （ ）1.经华东师范大学相关部门审查核定的“内部”或“涉密”学位论文 年 月 日解密， 后适用上述授权。
*，于 （
）2.不保密，适用上述授权。
导师签名
本人签名 年 月 日
* “涉密” 学位论文应是已经华东师范大学学位评定委员会办公室或保密委员会审定过的学 位论文（需附获批的《华东师范大学研究生申请学位论文“涉密”审批表》方为有效） ，未 经上述部门审定的学位论文均为公开学位论文。此声明栏不填写的，默认为公开学位论文， 均适用上述授权） 。
谭力 硕 位论文答辩委员会成员名单
姓名 孙 蕾 孙 强 章炯民 职称 副教授 副教授 副教授 单位 华东师范大学 机系 华东师范大学 机系 华东师范大学 机系 备注 主席
华东师范大学硕 位论文
基于情态演算的 UML 形式化验证与 OCL 约束自动生成研究
摘
要
从软件工程中软件生命周期的角度分析，软件架构是软件的核心结构与行 为，因而软件架构的设计是软件设 核心，也是随后进行代码开发的基础。因 此软件架构设 重要性不言而喻。由于软件架构设计本身是一种建模活动，如 何对软件架构设计的标准建模语言 UML 进行 '性验证是一个难题。传统软件 验证方法有着不够精 非自动化等不足。另外，对 UML 进行 '性验证需要 得到 UML 的形式化语义，而 UML 本身是一种图形化的表示方法，不具有形式 化的语义。因此本文将采用形式化方法来对 UML 模型进行形式化描述，即为其 赋予等价的形式化语义，再根据其语义进行形式化验证。为了进一步精确描述 UML 模型的语义，为其提供 OCL 约束是一种主流方法。而 OCL 约束需要人手 工编写，同样具有 '性难以保证、人员开销等问题，因此为 UML 模型自动生 成 OCL 约束模板是一种很好的 方法， 生成的 OCL 模板可供软件设计人员参 考，从而提高了软件工程的整体效率。本文也将对 OCL 约束自动生成进行研究。 UML 是软件设计过程事实上的标准建模语言。本文首先从历史发展、子图 种类、建模工具和以 XMI 表示的 UML 四个角度对 UML 作了简要的介绍，并具 体介绍了即将研究的两种 UML 子图：类图和状态图。同时介绍了形式化方法的 基本概念和主要分支，并总结了国内外现有的对 UML 形式化的研究。最后介绍 了 UML 的标准子语言 OCL、 采用的形式化语言情态演算和它的具体实现——逻 辑编程语言 Prolog，并进一步分析了从 UML 转换到情态演算的可行性，从理论 上 了给出的解决方案的 '性。 本文随后给出了基于情态演算的 UML 形式化描述方法。首先分析了选择 UML 类图和状态图作为研究对象的意义，再分别对 UML 类图和状态图进行形 式化描述：先是给出了两种子图的一种形式化语义结构；再分析了两种子图元素 与数理逻辑和情态演算元素的对应关系；又提出了两种子图到数理逻辑语句和 Prolog 的转换算法，并以伪代码的形式给出。然后着重定义了 UML 模型的 两种基本错误类型：领域无关的 UML 模型语法错误和领域相关的 UML 模型语 义错误，并给出具体错误实例和自动生成的 Prolog 。 进一步，本文讨论了如何实现对 UML 模型的 OCL 约束模板自动生成。首 先强调了 OCL 约束自动生成的研究意义，同时给出了 OCL 约束的应用范围。从 而进一步分析了如何在 UML 模型中提取 OCL 约束的目标应用对象，并给出了 一种提取算法。最后给出了该提取算法的 Perl 示例 的具体实现。 作为上述理论的补充和可行性证明，后续章节详细介绍了以 UML 子图到情 态演算的转换算法和 OCL 约束模板自动生成算法为基础而设计并实现的 UML

下一页