The term "formal methods" refers broadly to techniques for the verification and automatic synthesis of systems that satisfy desirable properties exactly or within some statistical tolerance. Historically developed for concurrent software, recent work has brought these methods to bear on motion planning in robotics. Challenges specific to robotics, such as uncertainty and real-time constraints, have motivated extensions and entirely novel treatments which draw on ideas from automata theory, logic, model checking, hybrid systems and control. However, compared to other areas of robotics research, demonstrations of formal methods have been surprisingly small-scale. In addition, there is a lack of benchmarks and metrics for evaluating novel algorithms.
This half-day workshop will bring together leading researchers in robotics, formal methods and hybrid systems, including those from industry. The discussions will be focused on metrics for evaluating the state of the art of formal methods for synthesis and verification of robotic systems, including the construction of appropriate benchmarks. This workshop will build on the success of its predecessors at ICRA 2009, 2010, CAV 2011, and RSS 2013, 2014. These previous events have tended toward broad inclusion of relevant work, motivated in part by the nascency of the field. We propose to focus this manifestation of the series at ICRA 2015 on benchmarks and metrics for evaluation. It will also provide a venue for discussing preparations and results from the First Challenge on Formal Methods for Robotics.
The workshop will take place during the morning of Saturday, 30 May 2015. Please beware that this agenda may change as we finalize workshop details. You may also want to consult the official schedule of workshops at ICRA 2015.
| 08:30-9:15 | Invited talk by Peter Trautman (Galois, Inc.): Formal methods at Galois Inc: current results, ongoing work, and future challenges |
| 09:15-10:00 | Invited talk by Eric Klavins (U. Washington): Reproducible experimental workflows though protocol programming languages |
| 10:00-10:30 | coffee |
| 10:30-11:00 | panel discussion |
| 11:00-11:16 | lightning talks |
| 11:16-11:20 | voting and organizing into SIGs |
| 11:20-11:45 | SIGs (a.k.a., "special interest groups" or "birds of a feather") |
| 11:45-12:00 | summaries about ideas and plans from SIGs |
Formal methods at Galois Inc: current results, ongoing work, and future challengesby Peter Trautman (Galois, Inc.):
Galois Inc. is a small software company that applies formal methods to computer science problems to build trustworthy systems. Historically, Galois has focused on “low-level” issues, such as cryptography, security, and software correctness. However, with the growing prevalence of automation in everyday systems, the need for “low-level” trustworthy systems has become imperative across a broad range of applications. In particular, Galois’ work on the DARPA program called High Assurance Cyber Military Systems (HACMS) resulted in the “world’s most secure UAV software”; additionally, common security vulnerabilities in modern automobiles and small UAVs were diagnosed and rectified using formal methods during this effort. Recently, Galois’ interest in formally verified robotics algorithms has grown, and we are currently exploring vulnerabilities in the ROS navigation stack, as well as high assurance human in the loop architectures. In general, an interesting research topic is simultaneously emerging from our software and robotics research teams: how does one apply formal methods to interacting probabilistic modules?
Reproducible experimental workflows though protocol programming languagesby Eric Klavins (U. Washington):
I will describe several recent efforts to standardize how protocols and workflows are specified using formal, executable programming languages. Writing protocols in these languages could lead to a revolution in how experimental work is done. I will then describe briefly my lab’s experience with Aquarium, our human-in-the-loop laboratory operating system that you can use to run experimental workflow programs reliably and reproducibly.