Verification of Autonomous Systems

Self-driving cars, robotic home assistants, medical robots and other diverse autonomous systems are becoming a worldwide reality. Consequently, verification of autonomous systems has become increasingly important, as in order for these systems to be adopted in everyday life, they must be deemed trustworthy and safe. From software engineering, to control systems design, we must ensure our autonomous systems are correct (with respect to design specifications) and do not posses a risk to users or third parties. Increasing efforts to propose methodologies and to develop tools related to the verification or verified design of autonomous systems can be encountered around the world. As technology progresses and the systems become more intricate and complex, with added intelligence and adaptive capabilities, the challenges of verification also diversify.

The aim of this one-day Workshop is two-fold.

• Taking stock and positioning ourselves. We will present the state-of-the-art in verification of autonomous systems, in terms of techniques, methodologies and successful applications. A key goal is to discuss the main challenges in verification, including the difficulty of defining meaningful requirements, highly unpredictable environments, interactions with people, and adaptation and learning mechanisms.
• Bringing together experts in verification with leading roboticists. We will motivate discussions to find common ground to address the verification challenges. We hope to open new avenues for future interdisciplinary collaboration amongst participants and expect that this will significantly advance the state-of-the-art.

Intended Audience:

• Researchers interested in exploring the space of research challenges in the verification of autonomous systems.
• Researchers and developers interested in verifying their autonomous robots.

Schedule

The event consisted of short panelist introductions and panel discussions on sub-topics. The live stream is available on YouTube.

SESSION 1: Research Opportunities and Current Challenges in Verification of Autonomous Systems

8:00-9:10   Panel: Signe Redfield, Leon Kester [slides (pdf)], Michael Fisher [slides (pdf)], Dejanira Araiza-Illan [slides (pdf)]

This session focuses on research opportunities and current challenges in verification of autonomous systems. Emergent robotics and autonomous systems industries impose new challenges in terms of complexity of both the systems to verify and the environments surrounding such systems. Practical approaches and tools need to address the verification challenges, at all systems levels and from the design stages to the ultimate software and hardware implementation.

Session 1 Notes (pdf)

SESSION 2: Verifying Human-Robot Interactions

9:10-10:20   Panel: Anders Sandberg [slides (pdf)], Spyros Maniatopoulos, Constance Heitmeyer, John Sustersic

This session focuses on the safety of human-robot interactions. Analysis of the implications of verification is necessary to address different individual and combined aspects of any system, at varying levels of autonomy. These aspects include the safety of the system and the safety of the humans and/or the environment, along with the ultimate functionality of the system. The levels of autonomy vary according to the applications, from unmanned vehicles, to robots assisting in household settings.

Session 2 Notes (pdf)

COFFEE BREAK - 10:20AM - 10:30AM

SESSION 3: Techniques for Practical Verification

10:30-11:30   Panel: Kerstin Eder, David Scheidt, Jim Woodcock [slides (pdf)], Jana Tumova [slides (pdf)]

This session focuses on methodologies and techniques for verification. The challenges of verifying autonomous systems call for the development of current and new methodologies and techniques to support practical verification tasks. Additionally, current approaches such as formal methods (model checking and theorem proving) and testing or simulation ought to be explored, separated, and/or combined, at different system control and structural levels. In this respect, we extend the scope of previous ICRA workshops that focused solely on formal methods.

Session 3 Notes (pdf)

SESSION 4: Ontologies: Translating from User Needs to Robot Behavior

11:30-12:30   Panel: Craig Schlenoff [slides (pdf)], Stephen Balakirsky [slides (pdf)], Jamie Lennon, Jacek Malec

This session focuses on requirements engineering and ontologies. Expressing the expected behaviors of robots and autonomous systems is fundamental for verification. The difficulty of this process increases when the systems adapt and learn over their lifetime. Ontologies to formulate requirements and systems’ specifications in the best possible manner are needed. Different languages and translation processes may also be needed, from human natural language to requirements for verification tasks.

Session 4 Notes (pdf)

Participation

Prior to the Workshop, attendance will be requested with two considerations in mind:

• We have invited participants from well established research networks, both academic and industry related, since they can provide greater insight to the current challenges of autonomous systems verification, and provide some real-life first-hand knowledge on a range of applications.
• We also invite early career researchers, including current graduate students, and postdoctoral researchers, and encourage the participation of persons new to the field of verification, such as robotics designers attending the main conference tracks at ICRA.

In terms of publicity and communications, we are pursuing the following courses of action:

• Personal invitations, via email, to academic and industry-based research networks and IEEE lists. These will include our own Verification of Autonomous Systems working group list as well as the Autonomous Intelligent Systems Partnership, the Robotics and Autonomous Systems Group and the EPSRC UK Network for Robotics and Autonomous Systems in the UK, the EURON mailing list in Europe, and various formal and informal international working groups like the NATO Research Task Group on Evaluating the Efficiency of Coordination Mechanisms for Distributed Mobile Sensors and ontology groups working towards IEEE standards. We expect that these invitations will also reach larger research groups in associated universities and institutions, and thus early career researchers.
• E-mails to relevant and more general robotics and verification networks mailing lists such as Robotics Worldwide Digest
• Distributing the Workshop's information through printed and printable resources. The Workshop's information will be formatted as a poster/flier, so that it can be printed and distributed to universities and companies across the world, and attached to the aforementioned e-mails.
• Call for panel participation, for up to two places in each session. The speakers and panel members will select from the applications, giving preference to early career researchers, such as recent PhD graduates and postdoctoral researchers with less than five years in the verification fields.
• Social media, including Facebook, Twitter, and blogs, to highlight the Workshop and to disseminate the web page link.
• An e-mail-based "question drop", to complement the discussions, as some interested parties will not be able to attend the workshop in person.

Furthermore, we will broadcast the Workshop live if the facilities are provided. If not, we plan to record the Workshop and upload the recording to YouTube. We will publish a written summary of the discussion outcomes to provide a posteriori engagement with both the verification and robotics research communities.

Registration

The workshop is over and registration is closed. To view the livestream, go here!

Interaction Among Participants

During the Workshop, we envision multiple types of interaction among participants over the course of the workshop.

• Formal interaction
  • Panelists will provide short summaries of their perspective
  • These perspectives will provide other participants with insightful ideas and questions to further the discussion
• Experienced:Early career interaction
  • Experienced researchers will interact with other early career researchers in the panels
  • Experienced and early career researchers will interact with participants of all levels through questions and discussions
• External interaction
  • Previously collected questions, from the suggested “question drop” format, will serve as a complement for the discussion, if the time constraints allow it
• Informal interaction
  • Moderators will actively encourage the participation of audience participants during the discussions
  • There will be a no-host lunch to encourage continued informal discussions between presenters, panelists, and attendees outside of the formal sessions
• Feedback
  • We will provide a paper feedback questionnaire to all the participants, to collect information on their perspective, according to their expertise. The questionnaire’s main objectives are to:
  • Determine the area of expertise and verification interests of the attendants to the Workshop: ontologies/requirements engineering, practical verification and validation of real-life systems, formal methods and formal-based frameworks (model checking, theorem proving, synthesis of controllers compliant to temporal logic properties), simulation/testing methods and frameworks, human-robot interaction (industrial, medical, home assistants), unmanned vehicle domain (aerial, ground, maritime, space), other robots or vehicles, control systems design, software engineering, perception, decision making, multi-robot systems, specific application areas.
  • Determine what is the most critical challenge to overcome in order to achieve a comprehensive and feasible verification of autonomous systems, in the area(s) of expertise of the participants.
  • Determine what is the most critical challenge to overcome in order to achieve a comprehensive and feasible verification of autonomous systems, in general, after they have listened to different discussions throughout the Workshop.
  • Collect any other questions that were not covered in the panels, to be raised in future meetings/workshops.

Support of an IEEE RAS Technical Committee

The proposed workshop is supported by the IEEE RAS Technical Committee on Performance Evaluation & Benchmarking of Robotic and Automation Systems (PEBRAS).

Contact

Workshop website hosted on robotistry.org