New Opportunities for Integrated Formal Methods

Mario Gleirscher; Simon Foster; Jim Woodcock

doi:10.1145/3357231

New Opportunities for Integrated Formal Methods

Mario Gleirscher, Simon Foster, Jim Woodcock

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

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.

Original language	English
Article number	117
Journal	ACM Computing Surveys
Volume	52
Issue number	16
DOIs	https://doi.org/10.1145/3357231
Publication status	Published - 23 Oct 2019

Bibliographical note

© 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.

Keywords

cs.SE
cs.CY
cs.RO

Access to Document

10.1145/3357231

1812_10103v3
© 2018
Submitted manuscript, 361 KBLicence: CC BY-NC-ND
1812_10103
© 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.
Accepted author manuscript, 457 KB

https://arxiv.org/abs/1812.10103

Cite this

@article{25a6aa42ca48411c9dc8aeae88ec14ce,

title = "New Opportunities for Integrated Formal Methods",

abstract = " 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. ",

keywords = "cs.SE, cs.CY, cs.RO",

author = "Mario Gleirscher and Simon Foster and Jim Woodcock",

note = "{\textcopyright} 2019. This is an author-produced version of the published paper. Uploaded in accordance with the publisher{\textquoteright}s self-archiving policy. Further copying may not be permitted; contact the publisher for details.",

year = "2019",

month = oct,

day = "23",

doi = "10.1145/3357231",

language = "English",

volume = "52",

journal = "ACM Computing Surveys",

publisher = "ACM",

number = "16",

}

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 -