Research output: Contribution to journal › Article › peer-review
New Opportunities for Integrated Formal Methods. / Gleirscher, Mario; Foster, Simon; Woodcock, Jim.
In: ACM Computing Surveys, Vol. 52, No. 16, 117, 23.10.2019.Research output: Contribution to journal › Article › peer-review
}
TY - JOUR
T1 - New Opportunities for Integrated Formal Methods
AU - Gleirscher, Mario
AU - Foster, Simon
AU - Woodcock, Jim
N1 - © 2019. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details.
PY - 2019/10/23
Y1 - 2019/10/23
N2 - Formal methods have provided approaches for investigating software engineering fundamentals and also have high potential to improve current practices in dependability assurance. In this article, we summarise known strengths and weaknesses of formal methods. From the perspective of the assurance of robots and autonomous systems~(RAS), we highlight new opportunities for integrated formal methods and identify threats to their adoption to be mitigated. Based on these opportunities and threats, we develop an agenda for fundamental and empirical research on integrated formal methods and for successful transfer of validated research to RAS assurance. Furthermore, we outline our expectations on useful outcomes of such an agenda.
AB - Formal methods have provided approaches for investigating software engineering fundamentals and also have high potential to improve current practices in dependability assurance. In this article, we summarise known strengths and weaknesses of formal methods. From the perspective of the assurance of robots and autonomous systems~(RAS), we highlight new opportunities for integrated formal methods and identify threats to their adoption to be mitigated. Based on these opportunities and threats, we develop an agenda for fundamental and empirical research on integrated formal methods and for successful transfer of validated research to RAS assurance. Furthermore, we outline our expectations on useful outcomes of such an agenda.
KW - cs.SE
KW - cs.CY
KW - cs.RO
U2 - 10.1145/3357231
DO - 10.1145/3357231
M3 - Article
VL - 52
JO - ACM Computing Surveys
JF - ACM Computing Surveys
IS - 16
M1 - 117
ER -