TY - GEN
T1 - Formal Methods Adoption in Industry
T2 - 18th International Colloquium on Theoretical Aspects of Computing , ICTAC 2021
AU - Tyler, Benjamin
N1 - Publisher Copyright:
© 2023, The Author(s), under exclusive licence to Springer Nature Switzerland AG.
PY - 2023
Y1 - 2023
N2 - While formal methods provide powerful means by which designers can show that their systems meet specific requirements, industry has been slow to adopt them. The need for users to learn specialized languages and have a firm grasp of mathematical logic are primary hurdles to such adoption. Even though formal verification tools can make the process less tedious and reduce human error, they generally still require guidance from humans with specialized knowledge. In this report, the author’s experiences working for a small business are presented, which involved the development and promotion of formal methods tools for public and government agencies. It is notable that the end users of these tools were not necessarily specialists, and often had little to no prior experience with formal methods. Here, we specifically look at the general-purpose design language that was used for modeling, the development of intuitive graphics-based tools to make the system design task easier, and how automated model checking was applied to the resulting system models. We discuss the interactions with and feedback from clients regarding these tools, and in the conclusion make some suggestions regarding their adoption.
AB - While formal methods provide powerful means by which designers can show that their systems meet specific requirements, industry has been slow to adopt them. The need for users to learn specialized languages and have a firm grasp of mathematical logic are primary hurdles to such adoption. Even though formal verification tools can make the process less tedious and reduce human error, they generally still require guidance from humans with specialized knowledge. In this report, the author’s experiences working for a small business are presented, which involved the development and promotion of formal methods tools for public and government agencies. It is notable that the end users of these tools were not necessarily specialists, and often had little to no prior experience with formal methods. Here, we specifically look at the general-purpose design language that was used for modeling, the development of intuitive graphics-based tools to make the system design task easier, and how automated model checking was applied to the resulting system models. We discuss the interactions with and feedback from clients regarding these tools, and in the conclusion make some suggestions regarding their adoption.
KW - Automated model checking
KW - Formal methods adoption
KW - Formal methods in industry
KW - Systems level design languages
UR - http://www.scopus.com/inward/record.url?scp=85177235606&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85177235606&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-43678-9_5
DO - 10.1007/978-3-031-43678-9_5
M3 - Conference contribution
AN - SCOPUS:85177235606
SN - 9783031436772
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 152
EP - 161
BT - Formal Methods for an Informal World - ICTAC 2021 Summer School, Virtual Event, Tutorial Lectures
A2 - Cerone, Antonio
PB - Springer Science and Business Media Deutschland GmbH
Y2 - 1 September 2021 through 7 September 2021
ER -