Chiari, M., Camilli, M., Bersani, M. M., van Beusekom, R., & Tamburri, D. A. (2025). Reality Check on Formal Methods in Industry: A Study of Verum Dezyne. JOURNAL OF SOFTWARE-EVOLUTION AND PROCESS, 37(12), Article 70069. https://doi.org/10.1002/smr.70069
E191-01 - Forschungsbereich Cyber-Physical Systems
-
Journal:
JOURNAL OF SOFTWARE-EVOLUTION AND PROCESS
-
ISSN:
2047-7473
-
Date (published):
Dec-2025
-
Number of Pages:
16
-
Publisher:
WILEY
-
Peer reviewed:
Yes
-
Keywords:
formal software engineering; formal verification; industry study
en
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.
en
Research Areas:
Computer Engineering and Software-Intensive Systems: 80% Information Systems Engineering: 10% Modeling and Simulation: 10%