A Satellite Workshop at Formal Methods 2019

This one day workshop will bring together researchers working on a range of techniques for formal verification or autonomous systems, to present recent work in the area, discuss key difficulties, and stimulate collaboration between the robotics and formal methods communities. This workshop will include invited speakers, contributed papers, experience reports, and a discussion panel.

Scope

Autonomous – and Robotic – Systems present unique challenges for formal methods. They are embodied entities that can interact with the real world and make autonomous decisions. Amongst others, they can be viewed as safety-critical, cyber-physical, hybrid, and real-time systems. Key issues for formal methods applied to autonomous systems include capturing how the system will deal with a dynamic external environment and verification of the system’s decision making capabilities – including planning, ethical, and reconfiguration choices. Some autonomous systems require certification before deployment, others require public trust for wide adoption; both of these scenarios are being tackled by formal methods.

The goals of this workshop are to bring together leading researchers in this area to present recent and ongoing work, including experience reports and case studies as well as identify future directions for this emerging application of formal methods. This workshop is concerned with the use of formal methods to specify, model, or verify autonomous or robotic systems; in whole or in part. Submissions may focus on case studies that identify the challenges for formal methods in this area, or experience reports that provide guidelines for tackling these challenges. Work using integrated formal methods, or describing the future directions of this field, are particularly welcome.

Programme Information

The workshop will feature invited speakers and presentations of accepted papers. The workshop will also feature a discussion panel for a structured, whole-group conversation for scoping the future directions of formal methods for autonomous systems.

Proceedings

The proceedings of FMAS2019 are available online, at the SpringerLink page for Part 1 of the proceedings of Formal Methods 2019 . Scroll about halfway down (or search “FMAS”) to find our section. The direct link to each paper is also available in the Accepted Papers list below.

Invited speakers

We had two invited speakers for FMAS.

  • Claudio Menghi , from the University of Luxembourg. Claudio’s research interests are in the field of formal methods and software engineering, with specific interests in cyber-physical systems, robotics, and formal verification.
  • Title : Formal Methods Meet Autonomous Systems:a Journey on a Two-Year Research Collaboration with Industry
  • Abstract : Autonomous - and Robotic - Systems are systems made up of collaborating computational elements, interacting and adapting to the physical environment and making autonomous decisions. Formal methods provide mathematically-based techniques for the specification and development of software and hard-ware systems. The adoption of formal methods by the industry developing autonomous and robotic systems is, however, still slow.This talk reports on a two-year research collaboration with industry focused on applying formal method techniques in the development of autonomous systems. First, it discusses the main challenges and results achieved in the definition of specification patterns for robotic missions, a project in collaboration with PAL Robotics and BOSCH. Mission specification patterns provide logic-based solutions for recurrent specification problems where developers have to define the desired behaviour of a robotic application (a.k.a missions). Then,it discusses a procedure for generating online test oracles from logic-based formulations of functional requirements of autonomous systems, a project in collaboration with Luxspace and QRA Corp. The procedure addresses a set of real-world challenges related to autonomous systems and has been evaluated on a real-world satellite system model. Finally, the talk presents a set of challenges and opportunities that emerged from the two-year journey of collaboration with industry
  • Kristin Y. Rozier , from Iowa State University. Kristin’s research interests cover a wide range of formal methods, including model checking and runtime verification, as well as system and safety health management for intelligent, autonomous Unmanned Aerial Systems.
  • Title : Runtime Reasoning that Really Flies
  • Abstract: Real-time, on-board runtime reasoning about system safety and security is required for autonomous systems, including most everything that flies: aircraft, spacecraft, satellites, and the robotic systems therein. The field of runtime verification (RV) is vast, and quickly growing, yet when it comes to real-life autonomous systems, current RV capabilities just don't fly. There is a dearth of RV tools that can operate within the constraints of real-life embedded operations that limit the system instrumentation, space, timing, power, weight, cost, operating conditions, and other resources. Even when we devise tools for embedded operation, RV must first clear the tall hurdles of input specifications, validation, verification, and flight certification. We highlight case studies where RV has recently risen to the occasion of reasoning on-board real-life autonomous systems, such as Unmanned Aerial Systems and NASA's Robonaut2, and examine the way up from here. What will it take for RV to really take off?

Accepted Papers

We accepted the following papers for FMAS 2019.

  • Authors: Keith Clark, Brijesh Dongol, and Peter Robinson.
  • Abstract: Teleo-Reactive (TR) procedures are a robotic agent programming language proposed by Nils Nilsson. Each parameterised procedure comprises a sequence of guarded action rules where the guards of later rules are sub-goals of the guard of the first rule. We informally describe the evaluation semantics of a TR procedure call. We then formalise the concept of a TR procedure call evaluation by expressing key properties in LTL. Finally we show how the LTL statements can be used to prove key properties of a simple TR program making use of assumptions about the correspondence between the agent’s Belief Store percept facts and properties of the perceived world, and between the agent’s actions and environment change.
  • Authors: Maike Schwammberger, and Christopher Bischopink
  • Abstract: Nowadays, autonomous crossing manoeuvres at intersections are especially challenging. In related work, a crossing controller for provably safe autonomous urban traffic manoeuvres was introduced. We extend this controller by a decentralised scheduling mechanism that ensures fair behaviour of the controller and also guarantees bounded liveness. We verify the correctness of our extension by an implementation and analysis with UPPAAL Stratego.
  • Authors: Andreas Nonnengart, Matthias Klusch, and Christian Mueller
  • Abstract: Ensuring pedestrian-safety is paramount to the acceptance and success of autonomous cars. The scenario-based training and testing of such self-driving vehicles in virtual driving simulation environments increasingly gained attention in the past years. Key challenge is the automated generation of critical traffic scenarios which usually are rare in real-world traffic, while computing and testing all possible scenarios is infeasible in practice. In this paper, we present a formal method-based approach CriSGen for an automated and complete generation of critical traffic scenarios for virtual training of self-driving cars. These scenarios are determined as close variants of given but uncritical and formally abstracted scenarios via reasoning on their non-linear arithmetic constraint formulas, such that the original maneuver of the self-driving car in them will not be pedestrian-safe anymore, enforcing it to further adapt the behavior during training.
  • Authors: Louis Viard, Laurent Ciarletta and Pierre-Etienne Moreau
  • Abstract: Safe operation of Cyber-Physical Systems such as Unmanned Aircraft Systems requires guarantees not only on the system, but also on the mission. Following approaches that are used to produce robust Cyber-Physical Controllers, we present the architecture of a mission definition, verification and validation toolchain. We conclude by reporting on the current state of the authors' implementation of this framework.
  • Authors: Gleifer Alves, Louise Dennis and Michael Fisher
  • Abstract: The design of autonomous vehicles includes obstacle detection and avoidance, route planning, speed control, etc. However, there is a gap considering how the rules of the road should be represented in an autonomous vehicle. Additionally, it is necessary to understand the behaviour of autonomous systems in order to check whether or not they work according to the rules of the road. Here, we propose a model checking agent-based architecture to embed the rules of the road in an agent representing the behaviour of an autonomous vehicle.

Submission Information

There were two categories of submission:

  • Short papers – 6 pages
  • Long papers – 15 pages

Topics of interest included (but are not limited to):

  • Experience reports/case studies on applying formal methods to autonomous and/or robotic systems
  • Novel formal methods that can be applied to autonomous and/or robotic systems
  • The modification of existing formal methods to suit autonomous and/or robotic systems
  • Future directions for formal methods for autonomous and/or robotic systems

Each submission received at least three, single-blind reviews. If a paper is accepted, at least one of the authors must attend the workshop to present their work. Revised selected papers will be published in the upcoming FM 2019 Workshops Lecture Notes in Computer Science volume. This will involve authors editing their papers based on the reviews and feedback at the workshop, which will then be reviewed again. The deadline for the LNCS volume is yet to be announced.

LNCS Logo

Important Dates

  • Submission: 30th June 2019 7th of July 2019 (AOE )
  • Notification: 31st July 2019 7th of August 2019
  • Final Version due: 1st September 2019
  • Workshop: 11th of October 2019 (at Formal Methods 2019 )

Organisers

Dr Marie Farrell , University of Liverpool, UK

Prof. Michael Fisher , University of Liverpool, UK
Dr Matt Luckcuck , University of Liverpool, UK

Programme Committee