https://www.dagstuhl.de/17071
February 12 – 17 , 2017, Dagstuhl Seminar 17071
Computer-Assisted Engineering for Robotics and Autonomous Systems
Organizers
Erika Abraham (RWTH Aachen, DE)
Hadas Kress-Gazit (Cornell University – Ithaca, US)
Lorenzo Natale (Italian Institute of Technology – Genova, IT)
Armando Tacchella (University of Genova, IT)
For support, please contact
Documents
Dagstuhl Report, Volume 7, Issue 2
Aims & Scope
List of Participants
Dagstuhl's Impact: Documents available
Dagstuhl Seminar Schedule [pdf]
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.


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