软件形式化方法

形式化方法将数学逻辑应用于软件的规约、开发和验证，使得系统属性能够被证明而非仅仅通过测试来验证。

Definition

形式化方法是基于数学的技术，用于规约、开发和验证软件系统，其中规约以形式化语言表达，属性通过证明或穷尽状态探索来确立。

Scope

本主题涵盖了形式化规约语言，如Z、B和TLA+；用于推理程序正确性的公理语义和霍尔逻辑；用于验证有限状态和并发系统的模型检测；定理证明和证明助手；以及形式化方法在安全关键和安保关键软件中的应用。

Core questions

• 如何用形式化语言明确地规约软件行为？
• 如何根据规约证明程序的正确性？
• 模型检测如何穷尽地验证有限状态和并发系统？
• 形式化方法的成本和效益在何种情况下能证明其使用的合理性？

Key theories

霍尔逻辑和公理语义

霍尔引入了一种前置条件和后置条件的逻辑，其中程序构造的正确性通过公理和推理规则表达，为证明程序符合其规约提供了基础。

模型检测

模型检测自动且穷尽地探索有限状态模型的可达状态，以验证时序逻辑属性，检测测试可能遗漏的死锁和违规。

Clinical relevance

形式化方法提供了最强的正确性保证，并应用于故障不可接受的领域——航空电子、铁路信号、安全协议和硬件——尽管其成本使其主要限于关键组件而非整个大型系统。

Evidence & guidelines

工业实践调查文件记录了形式化方法在安全关键领域成功应用，DO-178C和通用准则等标准在最高保证级别认可了形式化技术。

History

程序验证由Floyd和Hoare在1960年代后期创立，模型检测由Clarke、Emerson和Sifakis在1980年代早期开发（并因此获得了图灵奖），此后工具和证明助手使得形式化验证进入了关键系统的工业应用。

Debates

形式化方法的可扩展性和成本

一个持续的争论是形式化方法是否能经济地扩展到大型工业软件；自动化和轻量级形式化方法的进步拓宽了适用性，但大型系统的全面验证仍然成本高昂。

Key figures

• C. A. R. Hoare
• Edsger Dijkstra
• Edmund Clarke
• Leslie Lamport

Seminal works

• hoare1969
• clarke1999
• woodcock2009

Frequently asked questions

形式化方法是否取代测试？

通常不会。形式化方法对模型或规约提供强有力的保证，但假设、环境和未建模的方面仍需要测试；实践中两者是互补的，形式化方法侧重于最关键的属性。

为什么形式化方法没有被普遍使用？

它们需要专业的知识和精力，这对于大多数软件来说难以证明其合理性，因为测试能以较低成本提供足够的信心；形式化方法集中应用于故障后果严重到足以值得投资的领域。