arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2002.07279cs.SE
收藏

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

Formal Methods: From Academia to Industrial Practice. A Travel Guide

Marieke Huisman, Dilian Gurov, Alexander Malkis

AI总结:

本文探讨了形式化方法与工业实践之间差距依然存在的原因,建议通过提升工具易用性、改变利益相关者思维模式以及促进研究界合作来弥合该差距。

摘要:

几十年来,形式化方法一直被认为是帮助软件行业开发更可靠、更可信软件的可行途径。然而,尽管有这种强烈的信念和许多个人的成功故事,工业软件开发似乎并未发生真正的改变。事实上,软件行业本身正在快速向前发展,形式化方法所能实现的目标与日常软件开发实践之间的差距似乎并没有缩小(甚至可能还在扩大)。过去,为了缩小这一差距,人们已经就如何开展形式化方法研究提出了许多建议。本文探讨了为什么这一差距依然存在,并就形式化方法研究界可以做些什么来弥合该差距提出了自己的建议。我们的建议并不侧重于开放的研究问题。事实上,形式化方法的工具和技术已经具备很高的质量,能够解决许多非平凡的问题;我们确实提供了一些技术建议,说明如何使工具和技术更易于使用。在更大程度上,我们关注人的因素:如何产生影响,如何改变各利益相关者对此问题的思维方式,特别是作为一个研究界,如何改变我们的行为,从相互竞争转向合作来解决这一问题。

英文摘要:

For many decades, formal methods are considered to be the way forward to help the software industry to make more reliable and trustworthy software. However, despite this strong belief and many individual success stories, no real change in industrial software development seems to be occurring. In fact, the software industry itself is moving forward rapidly, and the gap between what formal methods can achieve and the daily software-development practice does not appear to be getting smaller (and might even be growing). In the past, many recommendations have already been made on how to develop formal-methods research in order to close this gap. This paper investigates why the gap nevertheless still exists and provides its own recommendations on what can be done by the formal-methods-research community to bridge it. Our recommendations do not focus on open research questions. In fact, formal-methods tools and techniques are already of high quality and can address many non-trivial problems; we do give some technical recommendations on how tools and techniques can be made more accessible. To a greater extent, we focus on the human aspect: how to achieve impact, how to change the way of thinking of the various stakeholders about this issue, and in particular, as a research community, how to alter our behaviour, and instead of competing, collaborate to address this issue.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑