Formal methods were frequently shown to be effective and, perhaps because of that, practitioners are interested in using them more often. Still, these methods are far less applied than expected, particularly, in critical domains where they are strongly recommended and where they have the greatest potential. Our hypothesis is that formal methods still seem not to be applicable enough or ready for their intended use. In critical software engineering, what do we mean when we speak of a formal method? And what does it mean for such a method to be applicable both from a scientific and practical viewpoint? Based on what the literature tells about the first question, with this manifesto, we lay out a set of principles that when followed by a formal method give rise to its mature applicability in a given scope. Rather than exercising criticism of past developments, this manifesto strives to foster an increased use of formal methods to the maximum benefit.
翻译:形式化方法已被多次证明是有效的,正因如此,从业者希望更频繁地使用它们。然而,这些方法的应用仍远低于预期,尤其在强烈推荐使用且潜力最大的关键领域中尤甚。我们的假设是,形式化方法似乎仍不够适用,或尚未准备好用于其预定用途。在关键软件工程中,当我们谈及形式化方法时究竟指什么?从科学和实践角度看,这样一种方法具有可用性又意味着什么?基于文献对第一个问题的阐述,我们在这份宣言中提出了一套原则:当形式化方法遵循这些原则时,便能在特定范围内实现成熟的适用性。本宣言并非对过去发展的批判,而是旨在促进形式化方法更广泛的应用,以最大限度地发挥其价值。