Thu 18 Jul 2019 16:40 - 17:00 at Mancy - Concurrency and Parallelism Chair(s): Stephen Kell

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 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.

Thu 18 Jul

ecoop-2019-papers
15:40 - 17:00: Research Papers - Concurrency and Parallelism at Mancy
Chair(s): Stephen KellUniversity of Kent
ecoop-2019-papers15:40 - 16:00
Research paper
Matthias SpringerTokyo Institute of Technology, Hidehiko MasuharaTokyo Institute of Technology
DOI Pre-print Media Attached
ecoop-2019-papers16:00 - 16:20
Research paper
Suvam MukherjeeMicrosoft Research India, Nitin John RajInternational Institute of Information Technology, Hyderabad, Krishnan GovindrajMicrosoft Research, Pantazis DeligiannisMicrosoft Research, Chandramouleswaran RavichandranMicrosoft Azure, Akash LalMicrosoft Research India, Aseem RastogiMicrosoft Research, Raja KrishnaswamyMicrosoft Azure
DOI Media Attached
ecoop-2019-papers16:20 - 16:40
Research paper
Jafar Haminimec-DistriNet, Depatrmant of Computer Science, KU Leuven, Belgium, Bart JacobsKU Leuven
DOI Media Attached
ecoop-2019-papers16:40 - 17:00
Research paper
Rupak MajumdarMPI-SWS, Germany, Marcus PirronMPI-SWS, Nobuko YoshidaImperial College London, Damien ZuffereyMPI-SWS
DOI Media Attached