Koord: A language for programming and verifying distributed robotics application

Ritwika Ghosh, Chiao Hsieh, Sasa Misailovic, Sayan Mitra

Research output: Contribution to journalArticlepeer-review

Abstract

A robot's code needs to sense the environment, control the hardware, and communicate with other robots. Current programming languages do not provide suitable abstractions that are independent of hardware platforms. Currently, developing robot applications requires detailed knowledge of signal processing, control, path planning, network protocols, and various platform-specific details. Further, porting applications across hardware platforms remains tedious. We present Koord-a domain specific language for distributed robotics-which abstracts platform-specific functions for sensing, communication, and low-level control. Koord makes the platform-independent control and coordination code portable and modularly verifiable. Koord raises the level of abstraction in programming by providing distributed shared memory for coordination and port interfaces for sensing and control. We have developed the formal executable semantics of Koord in the K framework. With this symbolic execution engine, we can identify assumptions (proof obligations) needed for gaining high assurance from Koord applications. We illustrate the power of Koord through three applications: formation flight, distributed delivery, and distributed mapping. We also use the three applications to demonstrate how platform-independent proof obligations can be discharged using the Koord Prover while platform-specific proof obligations can be checked by verifying the obligations using physics-based models and hybrid verification tools.

Original languageEnglish (US)
Article number232
JournalProceedings of the ACM on Programming Languages
Volume4
Issue numberOOPSLA
DOIs
StatePublished - Nov 13 2020

Keywords

  • Distributed Robotics
  • Programming Language for Robotics

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality

Fingerprint Dive into the research topics of 'Koord: A language for programming and verifying distributed robotics application'. Together they form a unique fingerprint.

Cite this