Separation of distributed coordination and control for programming reliable robotics

Ghosh, Ritwika

Permalink

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

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

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