Dr Matt Luckcuck and Prof. Michael Fisher, in collaboration with Dr Marie Farrell from the FAIR-SPACE Hub, organised an academic workshop on the robust verification and validation of autonomous systems. The workshop, entitled ‘Formal Methods for Autonomous Systems’ (FMAS) was held on the 11th of October at the Third World Congress on Formal Methods, in Porto.
Autonomous systems present a variety of challenges for robust verification and validation. FMAS featured presentations of research tackling how an autonomous robotic system copes with the unpredictable real world, how to provide evidence of the system’s adherence to safety rules, verification and validation of the system’s mission, and ensuring that the complex software that provides the system’s autonomy is correct.
FMAS had two invited speakers, who presented larger collections of work. Dr Claudio Menghi, from the University of Luxembourg, presented his two-year collaboration with industry, applying formal methods to autonomous systems. Dr Kristin Y. Rozier, from Iowa State University, presented her extensive work in developing runtime verification approaches for aircraft and aerospace systems, with a particular focus on how these techniques will work on resource-constrained embedded devices.
FMAS finished with a discussion session that included the two invited speakers and Prof Michael Fisher as panellists. The discussion, which had active input from the audience, covered: the challenges of applying formal methods to autonomous systems, the limitations of current formal verification methods, and how to introduce and embed formal methods into industry.
