形式化方法：从学术到工业实践——一份旅行指南

数十年来，形式化方法被视为帮助软件产业开发更可靠、可信软件的前进方向。然而，尽管有此坚定信念和许多个体成功案例，工业软件开发似乎并未发生真正改变。事实上，软件产业自身正快速前进，形式化方法所能达成与日常软件开发实践之间的鸿沟并未缩小（甚至可能扩大）。过去已提出许多关于如何开展形式化方法研究以缩小鸿沟的建议。本文探究该鸿沟为何依然存在，并给出我们自己的关于形式化方法研究界可采取何种行动来弥合它的建议。我们的建议不聚焦于开放研究问题。事实上，形式化方法工具与技术已具高质量并能解决诸多非平凡问题；我们确实给出了一些关于如何使工具与技术更易用的技术性建议。更大程度上，我们聚焦于人的因素：如何产生影响、如何改变各利益相关方对此问题的思维方式，尤其作为一个研究界，如何改变我们的行为，转而协作而非竞争以应对此问题。