苗德成，冯黎波

（1．韶关学院数学与信息科学学院，广东韶关 512000；2．河北科技大学理学院，河北石家庄 050018）

形式化方法在软件工程中的应用研究

苗德成1，冯黎波2

（1．韶关学院数学与信息科学学院，广东韶关 512000；2．河北科技大学理学院，河北石家庄 050018）

探讨了形式化方法的基本概念，重点研究了形式化方法的数学理论基础和其在软件工程各阶段的应用情况，分析了形式化方法在理论研究和工程实践上的优势和局限性及其原因，并指出了形式化方法发展的几个方向，最后对形式化方法在软件工程中的应用做了评价。

形式化方法；软件规约形式语言；软件工程；形式系统；规约

基于软件工程方法论，软件工程是将客观世界实际问题抽象成认识世界概念模型，再将认识世界概念模型转换为程序世界可执行程序集合的活动，前者是认知领域符号推演与系统论证过程，而后者则是工程领域理论实践与计算转换过程。在软件工程活动中成功运用形式化方法将实际问题认知模型转换为软件规约［1］（software specification）可缩短软件开发周期并减少项目研制成本，软件规约既是系统分析师、设计师、程序员与用户之间的协议，也是系统模块与程序部分的界面，只要保证软件规约对实际问题描述的可靠性与协调性，就能确保软件系统实现的完备性与一致性。

1 形式化方法

软件工程活动中形式化方法虽然被广泛使用，但形式语言、形式系统等相关基本概念并未有精确定义。……