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.
翻译:正规方法往往被证明是有效的,也许正统方法因此,从业人员对更经常地使用这些方法感兴趣;然而,这些方法的应用远远少于预期,特别是在大力推荐和具有最大潜力的关键领域。我们的假设是,正规方法似乎仍然不够适用,或不足以用于预定用途。在关键软件工程中,当我们谈论正式方法时,我们指的是什么?从科学和实际角度都适用这种方法意味着什么?根据文献对第一个问题(包括这一宣言)的描述,我们制定了一套原则,随后采用正式方法,在特定范围内使其成熟适用。这项宣言不是批评过去的发展,而是努力推动更多地使用正规方法,以获得最大利益。