形式化开发方法探索及应用

2023-10-25 理论教育版权反馈

【摘要】：20世纪80年代以来，形式化软件开发方法的研究及应用为解决上述问题找到了一条有效的途径，使用形式化方法开发软件可以提高软件的可读性、可靠性和可维护性以及软件的开发效率，并为实现软件开发的自动化奠定基础。软件开发的形式化方法是以一般形式化方法为基础的。它尤其适用于高安全性系统的开发，这也是形式化方法目前最主要的应用领域。另外，某些形式化方法缺乏描述软件结构的强有力机制，对大型软件的开发不太理想。

按传统软件开发方法设计与开发的软件产品，尤其是高可靠性的实时控制软件和军用软件（包括顺序、并行和实时软件）等大型软件系统，普遍存在着系统正确性及可靠性难以保证等问题，且难于实现软件自动化。20世纪80年代以来，形式化软件开发方法的研究及应用为解决上述问题找到了一条有效的途径，使用形式化方法开发软件可以提高软件的可读性、可靠性和可维护性以及软件的开发效率，并为实现软件开发的自动化奠定基础。

软件开发的形式化方法是以一般形式化方法为基础的。形式化方法为计算机系统的规约、实现和验证提供了合理的数学基础，首先对系统进行独立于实现的、基于一定形式化语义的抽象描述，然后经过逐步求精及变换，利用规约的数学特性检验其一致性，直至生成最终的软件系统。其优点在于它严格、精确地定义了用户需求，形式化规约的求精过程具有可推导、易证明的特性，从而有利于保证程序的正确性和实现软件自动化。它尤其适用于高安全性系统的开发，这也是形式化方法目前最主要的应用领域。但是，形式化方法要求使用者具有较好的数学背景，因而不便于最终用户参与开发过程，这阻碍了它的进一步发展。另外，某些形式化方法缺乏描述软件结构的强有力机制，对大型软件的开发不太理想。(www.chuimin.cn)

一个形式化的软件开发方法一般包括一套思维方法及描述方法、一种开发手段（如规范描述的原则、程序开发的一般过程、描述语言）和支持工具，使开发者能利用数学概念和表示方法恰当合理地构造形式规范，根据开发过程的框架及设计原则进行规范描述和系统化的设计求精，并使用证明的概念对规范的性质和设计步骤进行分析和验证。方法还应该有工具的支持，使开发过程可行且高效。

形式化开发方法探索及应用

相关推荐