Reality Check on Formal Methods in Industry: A Study of Verum Dezyne

Abstract

Many of the classical questions reflecting the actionable use of formal methods in the software industry—“do they scale?” or “are they easily integrated?”—remain without a definitive answer, with many potentially adoptable formal notations being exploited in industry, but in a rather stove-piped and siloed fashion, and with rather few, sometimes anecdotal, success stories to tell. In this article, we strive to provide some more answers to the aforementioned questions on formal methods adoption in industry. We focus our study on a widely adopted formal methods framework in Europe, that is, Verum Dezyne, employed by embedded-computing and hardware-programming companies including Thermo-Fisher, Philips, and more. Results convey a rather interesting story—requiring further study into these matters—but also highlight practical insights for formal practitioners in the field, for example, that formal methods do not disrupt existing processes and scalability issues can be easily addressed by applying mainstream engineering practices, such as decomposition.