Abstract: “Despite extensive evangelizing and demonstration of several success stories in safety-critical applications, formal methods are still not widely practiced in contemporary systems and software engineering. One of the main reasons for this situation is the absence of systematic guidelines and evaluation criteria that help software practitioners choose the right formal method for the problem at hand. In this article, we present a comprehensive set of criteria for evaluating and comparing different formal methods, based on a systematic literature review and decade-long personal experience with the application of formal methods in industrial projects. We argue that besides technical grounds (e.g., modeling capabilities and supported development phases), formal methods should also be evaluated from social and industrial perspectives. We also evaluate several state-based formal methods on the stipulated criteria.”
Most of the focus on formal methods community has been getting the logics to prove more components. They paid less attention to what’s usable by programmers, esp in industry. There’s also no criteria to evaluate that in a consistent way. Prior attempts were often dense works made for governments or paywalled. I really like that this author made an attempt at that with good questions to ask about each one. The author then rates several of them on those attributes. ASM’s and TLA+ come out as clear winners in usability and effectiveness.
I think this rating system and comparison needs some more attention by industrial users of formal methods and academics. People should be talking about what they like, don’t like, or just rating other methods similarly.
@minimax @joachimschipper @aminb @hwayne @dbp you all might find this useful or work with someone who would.