周建儒（四川信息职业技术学院，四川广元628040）



软件形式化建模方法探析

周建儒
（四川信息职业技术学院，四川广元628040）

摘要：传统软件开发流程存在各种缺陷。软件形式化方法是建立在严格数学基础上的软件开发方法，该方法为从根本上解决传统软件开发过程中存在的主要缺陷提供了可能，其中Pi验算就是比较典型的一种形式化语言，结合实例来分析Pi验算进行形式化建模的过程，可以帮助我们更好地了解这种形式化语言建模方式。

关键词：软件形式化；Pi验算；软件工程；建模方式

1　引言

在传统的软件开发中，往往会出现项目延迟、预算超支、后期发现软件缺陷等问题，从而花费高额代价进行修复。分析导致软件事故的诸多原因，我们发现很难从根本上解决软件开发方式所带来的问题，因为前期成果是用自然语言编写的文档，如需求规格说明书、设计说明书等，最后的成果是形式化的程序。文档是完全非形式化的表达，只能由人阅读和理解，难以通过自身的语义来证明其表达流程的正确性。而形式化的程序有严格的定义和语义［1］。程序的所有静态和动态性质都蕴藏在系统代码中，且程序包含过多的实现细节和语言细节，进行验证的成本很高。需求和设计与最终实现的程序的一致性难以判定［2］。测试发现问题的能力很有限，不能成为评判软件质量好坏的标准。因此，如果把前期的需求流程也完全通过严格的形式化语言来表述，那么会很容易保证需求和最终代码的一致性。……