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.
翻译:几十年来,正式方法被认为是帮助软件行业制造更可靠和更值得信赖的软件的前进道路。然而,尽管有这种强烈的信念和许多个别的成功事例,但工业软件开发似乎并没有发生真正的变化。事实上,软件行业本身正在迅速向前发展,正式方法所能达到的目标与日常软件开发实践之间的差距似乎并没有缩小(甚至可能扩大 ) 。过去,已经就如何发展正规方法研究以弥合这一差距提出了许多技术建议。本文探讨了为什么差距仍然存在,并就正式方法研究界可以做些什么提出自己的建议。我们的建议并不侧重于公开研究问题。事实上,正式方法工具和技术已经具有很高的质量,可以解决许多非技术性问题。我们确实就如何使工具和技术更容易获得提出了一些技术建议。我们更侧重于人类方面:如何实现影响,如何改变各利益相关方对这一问题的思维方式,如何改变我们的研究,特别是如何改变我们社区对这一问题的相互竞争,如何改变我们的研究,如何改变我们社区的行为。