A manifesto for applicable formal methods

TY - JOUR

T1 - A manifesto for applicable formal methods

AU - Gleirscher, Mario

AU - van de Pol, Jaco

AU - Woodcock, Jim

N1 - Publisher Copyright: © 2023, The Author(s).

PY - 2023/12

Y1 - 2023/12

N2 - Recently, formal methods have been used in large industrial organisations (including AWS, Facebook/Meta, and Microsoft) and have proved to be an effective part of a software engineering process finding important bugs. Perhaps because of that, practitioners are interested in using them more often. Nevertheless, formal methods are far less applied than expected, particularly for safety-critical systems where they are strongly recommended and have the most significant potential. We hypothesise that formal methods still seem not applicable enough or ready for their intended use in such areas. 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 identify key challenges and lay out a set of guiding 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 increased use of formal methods in any appropriate context to the maximum benefit.

AB - Recently, formal methods have been used in large industrial organisations (including AWS, Facebook/Meta, and Microsoft) and have proved to be an effective part of a software engineering process finding important bugs. Perhaps because of that, practitioners are interested in using them more often. Nevertheless, formal methods are far less applied than expected, particularly for safety-critical systems where they are strongly recommended and have the most significant potential. We hypothesise that formal methods still seem not applicable enough or ready for their intended use in such areas. 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 identify key challenges and lay out a set of guiding 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 increased use of formal methods in any appropriate context to the maximum benefit.

KW - Formal methods

KW - Formal verification

KW - Research evaluation

KW - Research transfer

KW - Software engineering

KW - Tools

UR - http://www.scopus.com/inward/record.url?scp=85168335655&partnerID=8YFLogxK

U2 - 10.1007/s10270-023-01124-2

DO - 10.1007/s10270-023-01124-2

M3 - Journal article

AN - SCOPUS:85168335655

SN - 1619-1366

VL - 22

SP - 1737

EP - 1749

JO - Software and Systems Modeling

JF - Software and Systems Modeling

IS - 6

ER -