New Opportunities for Integrated Formal Methods
This work addresses the problem of dependability assurance for robots and autonomous systems, but it is incremental as it builds on existing formal methods without introducing new techniques.
The paper identifies new opportunities for integrated formal methods in the assurance of robots and autonomous systems (RAS), summarizing known strengths and weaknesses, highlighting threats to adoption, and developing a research agenda for fundamental and empirical work.
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 the adoption of such methods. 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.