University of Illinois Urbana-Champaign

Separation of distributed coordination and control for programming reliable robotics

Ghosh, Ritwika

Content Files
GHOSH-DISSERTATION-2020.pdf

Permalink

https://hdl.handle.net/2142/108501

Description

Title
Separation of distributed coordination and control for programming reliable robotics
Author(s)
Ghosh, Ritwika
Issue Date
2020-07-16
Director of Research (if dissertation) or Advisor (if thesis)
Mitra, Sayan
Doctoral Committee Chair(s)
Mitra, Sayan
Committee Member(s)
  • Dullerud, Geir E
  • Johnson, Taylor T
  • Misailovic, Sasa
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Date of Ingest
2020-10-07T20:59:55Z
Keyword(s)
  • Programming Languages
  • Robotics
  • Distributed Systems
  • Formal Methods
  • Verification
Abstract
A robot's code needs to sense the environment, control the hardware, and communicate with other robots. Current programming languages do not provide the necessary hardware platform-independent abstractions, and therefore, developing robot applications require detailed knowledge of signal processing, control, path planning, network protocols, and various platform-specific details. Further, porting applications across hardware platforms becomes tedious. With the aim of separating these hardware dependent and independent concerns, we have developed Koord: a domain specific language for distributed robotics. Koord abstracts platform-specific functions for sensing, communication, and low-level control. Koord makes the platform-independent control and coordination code portable and modularly verifiable. It 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 proof obligations for gaining high assurance from Koord applications. Koord is deployed on CyPhyHouse---a toolchain that aims to provide programming, debugging, and deployment benefits for distributed mobile robotic applications. The modular, platform-independent middleware of CyPhyHouse implements these functionalities using standard algorithms for path planning (RRT), control (MPC), mutual exclusion, etc. A high-fidelity, scalable, multi-threaded simulator for Koord applications is developed to simulate the same application code for dozens of heterogeneous agents. The same compiled code can also be deployed on heterogeneous mobile platforms. This thesis outlines the design, implementation and formalization of the Koord language and the main components of CyPhyHouse that it is deployed on.
Graduation Semester
2020-08
Type of Resource
Thesis
Permalink
http://hdl.handle.net/2142/108501
Copyright and License Information
Copyright 2020 Ritwika Ghosh

Owning Collections

Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at Illinois
Dissertations and Theses - Computer Science
Dissertations and Theses from the Siebel School of Computer Science