数学和逻辑中把一个公式中的某个子项替换成另一个子项的操作过程就是项重写。项重写系统的理论是计算的基础理论。本文属于项重写技术在形式化方法领域的应用研究。主要贡献在于:成功地把项重写的基本思想应用在通用语言模型检测当中,给出基于通用语言源文件模型检测的思想框架和具体方案,并最终用实验表明这个方案的可行性。这项工作建立在对项重写系统概念背景和发展历史的考察基础上,借鉴了现代主流形式化工具的设计思想,并充分利用现代通用编程语言的高级特性,使得形式化建模更加容易。论文的全部工作包括:　　项重写技术用于系统规格和模型检测的实践现代软件技术的发展已经把项重写系统的理论用于软件实践,一些功能比较完备的基于重写技术的程序设计语言和工具已经被开发出来。使用这样的一种工具Maude在系统规格和模型检测方面做了一些实践:尝试用Maude表达Petri网模型,分析了软件形式化中Maude代替Petri网的可能性;使用Maude的search命令和LTL工具进行模型检测实践,并把模型检测方法用于求解智力游戏问题;参考别人代码基础上,完成了对简单微处理器建立Maude模型的实践。实践表明,基于重写技术的软件工具可以在一定程序上被当做通用编程语言使用,而不是仅仅作为软件形式化方法和软件测试中的专门技术。　　通用语言实现模型检测命令式语言和基于重写技术的语言(函数式语言)在其发展过程中都在向对方学习借鉴,取长补短。当今流行的一些命令式编程语言(如 Python)也有函数式编程的语法风格。尝试使用通用语言直接对源文件完成模型检测任务。结果表明,这种方法具有一定可行性。而使用通用语言完成形式化任务的优点在于:形式化测试可以集成到软件开发中,减少由于软件形式方法带来的额外成本。程序员不必为了模型检测去专门学习新语言。