Thu 18 Jul 2019 16:40 - 17:00 at Track 1 - Concurrency and Parallelism

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

15:40 - 17:00: ECOOP Research Papers - Concurrency and Parallelism at Track 1
ecoop-2019-papers15:40 - 16:00
Research paper
Matthias SpringerTokyo Institute of Technology, Hidehiko MasuharaTokyo Institute of Technology
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
ecoop-2019-papers16:20 - 16:40
Research paper
Jafar Haminimec-DistriNet, Depatrmant of Computer Science, KU Leuven, Belgium, Bart JacobsKU Leuven
ecoop-2019-papers16:40 - 17:00
Research paper
Rupak MajumdarMPI-SWS, Germany, Marcus PirronMPI-SWS, Nobuko YoshidaImperial College London, Damien ZuffereyMPI-SWS