Files in this item

FilesDescriptionFormat

application/pdf

application/pdfGHOSH-DISSERTATION-2020.pdf (6MB)
(no description provided)PDF

Description

Title:Separation of distributed coordination and control for programming reliable robotics
Author(s):Ghosh, Ritwika
Director of Research:Mitra, Sayan
Doctoral Committee Chair(s):Mitra, Sayan
Doctoral Committee Member(s):Dullerud, Geir E; Johnson, Taylor T; Misailovic, Sasa
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Degree:Ph.D.
Genre:Dissertation
Subject(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.
Issue Date:2020-07-16
Type:Thesis
URI:http://hdl.handle.net/2142/108501
Rights Information:Copyright 2020 Ritwika Ghosh
Date Available in IDEALS:2020-10-07
Date Deposited:2020-08


This item appears in the following Collection(s)

Item Statistics