TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 17071

Computer-Assisted Engineering for Robotics and Autonomous Systems

( Feb 12 – Feb 17, 2017 )


Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/17071

Organizers

Contact



Schedule

Motivation

An autonomous system is a system which performs certain intended tasks based on its current state and sensing, without human supervision. There are several fields in which autonomous systems play an increasing role like, e.g., aerospace, railway signaling or automotive engineering.

In the absence of external control, it is highly important to make sure that autonomous systems are functionally safe. The more critical system safety is, the more important is to introduce standardized certifications to assure their correct functioning. However, though au- tonomous systems are increasingly involved in our everyday life, both exact formalizations of safe functionality (standards, what we want to be confident in), and methods to achieve confi- dence (methodologies, how we get confident in the properties we want to assure) are still scarce and not well integrated.

To move towards the initiation of such standards and the development of such technologies, in this seminar we want to discuss at an abstract level (1) what are general safety requirements for autonomous systems, (2) what are potential key technologies that could be employed to assure that those safety requirements hold, and (3) what are the obstacles on the way to the application of those technologies.

Robotics is a typical area for the development of Autonomous Systems . As models are a basic requirement for the formal analysis of systems, Model-driven Software Engineering plays an important role to enable the application of Formal Methods. With this seminar we would like to bring together these communities to exchange knowledge, opinions and needs, to develop recommendations, and to initiate road maps to increase the safety of autonomous systems.

In the above communities, a plethora of interesting activities and innovative results can be observed, however, without close connections between the different areas. For example in Robotics, Model-driven Software Engineering methods are still seldomly used, and even when they are applied, the approaches are not general, i.e., not directly transferable to other ap- plication domains. Also Model-driven Software Engineering and Formal Methods are not well connected, e.g., novel results in hardware/software verification are not directly transferred to Model-driven Software Engineering technologies. As Formal Methods need formal models of the systems of interest, Model-driven Software Engineering could build a bridge between Robotics and Formal Methods, being an enabling condition for the application of Formal Methods to Autonomous Systems.

Copyright Erika Abraham, Hadas Kress-Gazit, Lorenzo Natale, and Armando Tacchella

Summary

This seminar focused on autonomous systems, and more specifically robots, that operate without, or with little, external supervision. For these systems to be integrated into society, it is highly important to make sure that they are functionally safe. Formal Methods are techniques adopted in engineering for the verification of software and hardware systems. As models are a basic requirement for the formal analysis of systems, Model-driven Software Engineering plays an important role to enable the application of Formal Methods. Though autonomous systems are increasingly involved in our everyday life, both exact formalizations of safe functionality (standards, what we want to be confident in) and methods to achieve confidence (methodologies, how we get confident in the properties we want to assure) are still scarce. This seminar brought together experts in Artificial Intelligence and Robotics, Model-driven Software Engineering, and Formal Methods. It included researchers from academia as well as from industry. The following list summarizes high-level themes that emerged from the seminar:

  • Dealing with highly complex systems, it is difficult to verify or even model all aspects of the system, therefore focusing effort on efficient falsification rather than costly verification can be highly impactful for industrial applications.
  • The community can and should leverage results and systems built for different robotic competitions to reason about possible requirements and techniques to verify/falsify them. These competitions include the DARPA robotics challenge, the Amazon picking challenge, different leagues in Robocup, etc. Creating benchmarks based on these competitions will enable progress in verification of autonomous systems.
  • Creating small interdisciplinary teams that include people from formal methods, robotics and model based design that tackle small yet realistic problems, possibly inspired by industrial applications, will help formalize the language of requirements, models and verification techniques that will have an impact on autonomous systems.
Copyright Erika Abraham, Hadas Kress-Gazit, Lorenzo Natale, and Armando Tacchella

Participants
  • Erika Abraham (RWTH Aachen, DE) [dblp]
  • Jan Broenink (University of Twente, NL) [dblp]
  • Simon Burton (Robert Bosch GmbH - Stuttgart, DE) [dblp]
  • Pablo Bustos (University of Extremadura - Cáceres, ES) [dblp]
  • Alessandro Cimatti (Bruno Kessler Foundation - Trento, IT) [dblp]
  • Manuel Alcino Cunha (INESC TEC - Porto, PT & University of Minho - Braga, PT) [dblp]
  • Kerstin I. Eder (University of Bristol, GB) [dblp]
  • Rüdiger Ehlers (Universität Bremen, DE) [dblp]
  • Samira Farahani (MPI-SWS - Kaiserslautern, DE) [dblp]
  • Stefano Ghidoni (University of Padova, IT) [dblp]
  • Christoffer R, Heckman (University of Colorado - Boulder, US) [dblp]
  • Christian Heinzemann (Robert Bosch GmbH - Stuttgart, DE) [dblp]
  • Holger Hermanns (Universität des Saarlandes, DE) [dblp]
  • Felix Ingrand (LAAS - Toulouse, FR) [dblp]
  • Nils Jansen (Univ. of Texas at Austin, US) [dblp]
  • Joost-Pieter Katoen (RWTH Aachen, DE) [dblp]
  • Hadas Kress-Gazit (Cornell University - Ithaca, US) [dblp]
  • Jan Kretinsky (TU München, DE) [dblp]
  • Morteza Lahijanian (University of Oxford, GB) [dblp]
  • Gerhard Lakemeyer (RWTH Aachen, DE) [dblp]
  • Ratan Lal (Kansas State University - Manhattan, US) [dblp]
  • Martin Leucker (Universität Lübeck, DE) [dblp]
  • Ingo Lütkebohle (Robert Bosch GmbH - Stuttgart, DE) [dblp]
  • Daniele Magazzeni (King's College London, GB) [dblp]
  • Björn Matthias (ABB AG Forschungszentrum - Ladenburg, DE) [dblp]
  • Lorenzo Natale (Italian Institute of Technology - Genova, IT) [dblp]
  • Sandeep Neema (DARPA - Arlington, US) [dblp]
  • Petter Nilsson (University of Michigan - Ann Arbor, US) [dblp]
  • Shashank Pathak (Technion - Haifa, IL) [dblp]
  • Subramanian Ramamoorthy (University of Edinburgh, GB) [dblp]
  • Vasumathi Raman (Zoox Inc., US) [dblp]
  • Kristin Yvonne Rozier (Iowa State University, US) [dblp]
  • Christian Schlegel (Hochschule Ulm, DE) [dblp]
  • Maria Svorenova (University of Oxford, GB) [dblp]
  • Armando Tacchella (University of Genova, IT) [dblp]
  • Sebastian Wrede (Universität Bielefeld, DE) [dblp]

Classification
  • artificial intelligence / robotics
  • software engineering
  • verification / logic

Keywords
  • Autonomous Systems
  • Artificial Intelligence
  • Robotics
  • Computer-aided Software Development
  • Domain-specific Languages
  • Model-driven Software Engineering
  • Safety
  • Testing
  • Analysis
  • Verification
  • Synthesis
  • Formal Methods