|
Published: 21st October 2021 DOI: 10.4204/EPTCS.348 ISSN: 2075-2180 |
Autonomous systems are highly complex and present unique challenges for the application of formal methods. Autonomous systems act without human intervention, and are often embedded in a robotic system, so that they can interact with the real world. As such, they exhibit the properties of safety-critical, cyber-physical, hybrid, and real-time systems.
This EPTCS volume contains the proceedings for the third workshop on Formal Methods for Autonomous Systems (FMAS 2021), which was held virtually on the 21st and 22nd of October 2021. Like the previous workshop, FMAS 2021 was an online, stand-alone event, as an adaptation to the ongoing COVID-19 restrictions. Despite the challenges this brought, we were determined to build on the success of the previous two FMAS workshops.
The goal of FMAS is to bring together leading researchers who are tackling the unique challenges of autonomous systems using formal methods, to present recent and ongoing work. We are interested in the use of formal methods to specify, model, or verify autonomous and/or robotic systems; in whole or in part. We are also interested in successful industrial applications and potential future directions for this emerging application of formal methods.
As in previous years, FMAS 2021 encouraged the submission of both long and short papers. In total, we received 18 papers – 9 long papers and 9 short papers – from authors in Brazil, France, Germany, Iran, Italy, Norway, Slovakia, the United Kingdom, and the United States of America. This was a fantastic number of papers for FMAS, more than the number of submissions from the previous two workshops put together. Each paper received three reviews, and we accepted 12 papers in total: 8 long papers and 4 short papers.
FMAS 2021 hosted two invited speakers. Clare Dixon, from the University of Manchester, was invited to talk about "Help or Hazard: Towards Verifying Autonomous Robot Systems". Divya Gopinath, from the Robust Software Engineering (RSE) group at the NASA Ames Research Center, was invited to talk about "Understanding and Verifying Deep Neural Networks".
We would like to thank our brilliant programme committee who have once again delivered detailed and constructive reviews to the authors, despite the ongoing disruption and stress caused by the COVID-19 pandemic. We're proud to have such an enthusiastic collection of reviewers, and we want to thank them for their time and effort – especially with the unexpected number of submissions to FMAS 2021. We would like to thank our invited speakers, Clare Dixon and Divya Gopinath; the authors who submitted papers; our EPTCS editor, Martin Wirsing; and all of the attendees this year.
Marie Farrell and Matt Luckcuck,
Department of Computer Science, Maynooth University, Ireland
Autonomous robotic systems are being developed to operate in a range of environments: industrial, transport, healthcare and domestic and have the potential to be of great benefit to society. Further, they may be assisting, collaborating with or working near humans. We must make sure they are safe, robust, reliable and trustworthy and they themselves don't become become the hazard. In this talk I will discuss ways to verify such systems, relating to research carried out over a number of projects with different types of robot, operating in a range of scenarios.
Acknowledgements
Deep Neural Networks (DNNs) have gained immense popularity in recent times and have widespread use in applications such as image classification, sentiment analysis, speech recognition and also in safety-critical applications such as autonomous driving. However, they suffer limitations such as lack of explainability and robustness which raise safety and security concerns in their usage. Further, the complex structure and large input spaces of DNNs act as an impediment to thorough verification and testing. The SafeDNN project at the Robust Software Engineering (RSE) group at NASA aims at exploring techniques to ensure that systems that use deep neural networks are safe, robust and interpretable. In this talk, I would be presenting our technique Prophecy[1] that automatically infers formal properties of deep neural network models. The tool extracts patterns based on neuron activations as preconditions that imply certain desirable output properties of the model. I would be highlighting case studies that use Prophecy in obtaining explanations for network decisions, understanding correct and incorrect behavior, providing formal guarantees with respect to safety and robustness, and debugging neural network models. We have applied the tool on image classification networks, neural network controllers providing turn advisories in unmanned aircrafts, regression models used for autonomous center-line tracking in aircrafts and neural network object detectors.