基于项重写技术的规格和模型检测研究-计算机软件与理论专业论文.docx

万方数据 万方数据 独创性（或创新性）声明 本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究 成果。尽我所知，除了文中特别加以标注和致谢中所罗列的内容以外，论文中不包 含其他人已经发表或撰写过的研究成果；也不包含为获得桂林电子科技大学或其它 教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何 贡献均已在论文中做了明确的说明并表示了谢意。 申请学位论文与资料若有不实之处，本人承担一切相关责任。 本人签名： 日期： 关于论文使用授权的说明 本人完全了解桂林电子科技大学有关保留和使用学位论文的规定，即：研究生 在校攻读学位期间论文工作的知识产权单位属桂林电子科技大学。本人保证毕业离 校后，发表论文或使用论文工作成果时署名单位仍然为桂林电子科技大学。学校有 权保留送交论文的复印件，允许查阅和借阅论文；学校可以公布论文的全部或部分 内容，可以允许采用影印、缩印或其它复制手段保存论文。（保密的论文在解密后 遵守此规定） 本学位论文属于保密在 年解密后适用本授权书。 本人签名： 日期： 导师签名： 日期： 摘要 摘要 摘要 数学和逻辑中把一个公式中的某个子项替换成另一个子项的操作过程就是项重写。项重写 系统的理论是计算的基础理论。本文属于项重写技术在形式化方法领域的应用研究。主要贡献 在于：成功地把项重写的基本思想应用在通用语言模型检测当中，给出基于通用语言源文件模 型检测的思想框架和具体方案，并最终用实验表明这个方案的可行性。这项工作建立在对项重 写系统概念背景和发展历史的考察基础上，借鉴了现代主流形式化工具的设计思想，并充分利 用现代通用编程语言的高级特性，使得形式化建模更加容易。论文的全部工作包括： 项重写技术用于系统规格和模型检测的实践 现代软件技术的发展已经把项重写系统的理 论用于软件实践，一些功能比较完备的基于重写技术的程序设计语言和工具已经被开发出来。 使用这样的一种工具 Maude 在系统规格和模型检测方面做了一些实践：尝试用 Maude 表达 Petri 网模型，分析了软件形式化中 Maude 代替 Petri 网的可能性；使用 Maude 的 search 命令和 LTL 工具进行模型检测实践，并把模型检测方法用于求解智力游戏问题；参考别人代码基础上，完 成了对简单微处理器建立 Maude 模型的实践。实践表明，基于重写技术的软件工具可以在一定 程序上被当做通用编程语言使用，而不是仅仅作为软件形式化方法和软件测试中的专门技术。 通用语言实现模型检测 命令式语言和基于重写技术的语言（函数式语言）在其发展过程 中都在向对方学习借鉴，取长补短。当今流行的一些命令式编程语言(如 Python)也有函数式编 程的语法风格。尝试使用通用语言直接对源文件完成模型检测任务。结果表明，这种方法具有 一定可行性。而使用通用语言完成形式化任务的优点在于：形式化测试可以集成到软件开发中， 减少由于软件形式方法带来的额外成本。程序员不必为了模型检测去专门学习新语言。 关键字：项重写技术 模型检测 通用语言模型检测 形式化方法, Python I Abstract Abstract II万方数据 II 万方数据 Abstract In mathematics and logic area, the operation of substituting new terms for old ones is called term rewriting. The theory of term rewriting systems is the basic theory of computation. This article is about application studies on formal method based on term rewriting technologies, and the main contributions are: Basic ideas of term rewriting are successfully used in usual model checking, and a general framework and detailed scheme is given, which is proved as feasible with further experiments. This development work is based on a good study of the concept, background and development history of term rewriting systems. The design philosophies behind