Motion session types for robotic interactions
File(s)
Published version
Author(s)
Yoshida, Nobuko
Majumdar, Rupak
Pirron, Marcus
Zufferey, Damien
Type
Conference Paper
Abstract
Robotics applications involve programming concurrent components synchronising through messages while simultaneously executing motion primitives that control the state of the physical world. Today, these applications are typically programmed in low-level imperative programming languages which provide little support for abstraction or reasoning. We present a unifying programming model for concurrent message-passing systems that additionally control the evolution of physical state variables, together with a compositional reasoning framework based on multiparty session types. Our programming model combines message-passing concurrent processes with motion primitives. Processes represent autonomous components in a robotic assembly, such as a cart or a robotic arm, and they synchronise via discrete messages as well as via motion primitives. Continuous evolution of trajectories under the action of controllers is also modelled by motion primitives, which operate in global, physical time. We use multiparty session types as specifications to orchestrate discrete message-passing concurrency and continuous flow of trajectories. A global session type specifies the communication protocol among the components with joint motion primitives. A projection from a global type ensures that jointly executed actions at end-points are communication safe and deadlock-free, i.e., session-typed components do not get stuck. Together, these checks provide a compositional verification methodology for assemblies of robotic components with respect to concurrency invariants such as a progress property of communications as well as dynamic invariants such as absence of collision. We have implemented our core language and, through initial experiments, have shown how multiparty session types can be used to specify and compositionally verify robotic systems implemented on top of off-the-shelf and custom hardware using standard robotics application libraries.
Date Issued
2019-07-01
Date Acceptance
2019-04-01
Citation
LIPIcs : Leibniz International Proceedings in Informatics, 2019, 134, pp.28:1-28:27
ISBN
978-3-95977-111-5
ISSN
1868-8969
Publisher
Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
Start Page
28:1
End Page
28:27
Journal / Book Title
LIPIcs : Leibniz International Proceedings in Informatics
Volume
134
Copyright Statement
©Rupak Majumdar, Marcus Pirron, Nobuko Yoshida, and Damien Zufferey;licensed under Creative Commons License CC-BY (https://creativecommons.org/licenses/by/3.0/)
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Grant Number
ERI 025567 (EP/K034413/1)
PO 20015393
EP/K011715/1
EP/N027833/1
PO 20015391
Source
European Conference on Object-Oriented Programming
Publication Status
Published
Start Date
2019-07-15
Finish Date
2019-07-19
Coverage Spatial
London, UK