Formal Methods in Industry
Formal methods encompass a wide choice of techniques and tools for the specification, development, analysis, and verification of software and hardware systems. Formal methods are widely applied in industry, in activities ranging from the elicitation of requirements and the early design phases all the way to the deployment, configuration, and runtime monitoring of actual systems. Formal methods allow one to precisely specify the environment in which a system operates, the requirements and properties that the system should satisfy, the models of the system used during the various design steps, and the code embedded in the final implementation, as well as to express conformance relations between these specifications. We present a broad scope of successful applications of formal methods in industry, not limited to the well-known success stories from the safety-critical domain, like railways and other transportation systems, but also covering other areas such as lithography manufacturing and cloud security in e-commerce, to name but a few. We also report testimonies from a number of representatives from industry who, either directly or indirectly, use or have used formal methods in their industrial project endeavours. These persons are spread geographically, including Europe, Asia, North and South America, and the involved projects witness the large coverage of applications of formal methods, not limited to the safety-critical domain. We thus make a case for the importance of formal methods, and in particular of the capacity to abstract and mathematical reasoning that are taught as part of any formal methods course. These are fundamental Computer Science skills that graduates should profit from when working as computer scientists in industry, as confirmed by industry representatives.
Authors
- Roderick Chapman (ORCID: https://orcid.org/0000-0003-2717-760X)
- Jeroen J. A. Keiren (ORCID: https://orcid.org/0000-0002-5772-9527)
- Rance Cleaveland (ORCID: https://orcid.org/0000-0002-4952-5380)
- Hubert Garavel
- Cristina Seceleanu (ORCID: https://orcid.org/0000-0003-2870-2680)
- Thierry Lecomte (ORCID: https://orcid.org/0000-0001-8977-4827)
- Augusto Sampaio (ORCID: https://orcid.org/0000-0001-6593-577X)
- Tim A. C. Willemse (ORCID: https://orcid.org/0000-0003-3049-7962)
- Martyn Thomas (ORCID: https://orcid.org/0000-0003-1226-2772)
- Kristin Yvonne Rozier (ORCID: https://orcid.org/0000-0002-6718-2828)
- Michaël Leuschel (ORCID: https://orcid.org/0000-0002-4595-1518)
- Maurice H. ter Beek (ORCID: https://orcid.org/0000-0002-2930-6367)
- Rong Gu (ORCID: https://orcid.org/0000-0003-0570-6005)
- Lijun Zhang (ORCID: https://orcid.org/0000-0002-3692-2088)
- Ivo ter Horst (ORCID: https://orcid.org/0009-0003-2655-2698)
Institutions
- Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo" (IT)
- Institut national de recherche en sciences et technologies du numérique (FR)
- Mt. Hood Community College (US)
- Iowa State University (US)
- Chinese Academy of Sciences (CN)
- Universidade Federal de Pernambuco (BR)
- Amazon (United Kingdom) (GB)
- Institute of Software (CN)
- Heinrich Heine University Düsseldorf (DE)
- University of Maryland, College Park (US)
- Barnardo's (GB)
- Mälardalen University (SE)
- Eindhoven University of Technology (NL)
- ASML (Netherlands) (NL)
Publication Details
- Journal
- Formal Aspects of Computing
- Published
- 2024-08-21
- DOI
- https://doi.org/10.1145/3689374
- Citations
- 58
- Primary Topic
- Formal Methods in Verification
- Type
- article
- Field-Weighted Citation Impact
- 20.96