{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/108501"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/108501","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Separation of distributed coordination and control for programming reliable robotics","abstract":"Made available in DSpace on 2020-10-07T20:59:55Z (GMT). No. of bitstreams: 2 GHOSH-DISSERTATION-2020.pdf: 5711274 bytes, checksum: 60801584e32a9632d4bd7bfd1743e6c5 (MD5) LICENSE.txt: 4210 bytes, checksum: f2dc51ebbf42efab5e722f4638193a7a (MD5) Previous issue date: 2020-07-16","abstract_html":"Made available in DSpace on 2020-10-07T20:59:55Z (GMT). No. of bitstreams: 2 GHOSH-DISSERTATION-2020.pdf: 5711274 bytes, checksum: 60801584e32a9632d4bd7bfd1743e6c5 (MD5) LICENSE.txt: 4210 bytes, checksum: f2dc51ebbf42efab5e722f4638193a7a (MD5) Previous issue date: 2020-07-16","abstract_has_math":false,"creators":["Ghosh, Ritwika"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Mitra, Sayan","Dullerud, Geir E","Johnson, Taylor T","Misailovic, Sasa"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2020,"date_issued":"2020-10-07T20:59:55Z","date_published":"2020-10-07T20:59:55Z","updated_at":"2026-07-22T22:24:48Z","subjects":["Programming Languages","Robotics","Distributed Systems","Formal Methods","Verification"],"languages":["en"],"rights":["Copyright 2020 Ritwika Ghosh"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/108501","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Mitra, Sayan","Dullerud, Geir E","Johnson, Taylor T","Misailovic, Sasa"]},{"key":"dc:creator","label":"Author","values":["Ghosh, Ritwika"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2020-10-07T20:59:55Z","2020-07-16","2020-08"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Programming Languages","Robotics","Distributed Systems","Formal Methods","Verification"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2020 Ritwika Ghosh"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/108501"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Made available in DSpace on 2020-10-07T20:59:55Z (GMT). No. of bitstreams: 2 GHOSH-DISSERTATION-2020.pdf: 5711274 bytes, checksum: 60801584e32a9632d4bd7bfd1743e6c5 (MD5) LICENSE.txt: 4210 bytes, checksum: f2dc51ebbf42efab5e722f4638193a7a (MD5) Previous issue date: 2020-07-16","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.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2020-10-02 without embargo terms","The student, Ritwika Ghosh, accepted the attached license on 2020-07-15 at 17:46.","The student, Ritwika Ghosh, submitted this Dissertation for approval on 2020-07-15 at 17:59.","This Dissertation was approved for publication on 2020-07-16 at 14:37.","DSpace SAF Submission Ingestion Package generated from Vireo submission #15638 on 2020-10-02 at 15:13:55"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Separation of distributed coordination and control for programming reliable robotics"]}]}],"canonical_facts":{"dc:contributor":["Mitra, Sayan","Dullerud, Geir E","Johnson, Taylor T","Misailovic, Sasa"],"dc:creator":["Ghosh, Ritwika"],"dc:date":["2020-10-07T20:59:55Z","2020-07-16","2020-08"],"dc:description":["Made available in DSpace on 2020-10-07T20:59:55Z (GMT). No. of bitstreams: 2 GHOSH-DISSERTATION-2020.pdf: 5711274 bytes, checksum: 60801584e32a9632d4bd7bfd1743e6c5 (MD5) LICENSE.txt: 4210 bytes, checksum: f2dc51ebbf42efab5e722f4638193a7a (MD5) Previous issue date: 2020-07-16","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.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2020-10-02 without embargo terms","The student, Ritwika Ghosh, accepted the attached license on 2020-07-15 at 17:46.","The student, Ritwika Ghosh, submitted this Dissertation for approval on 2020-07-15 at 17:59.","This Dissertation was approved for publication on 2020-07-16 at 14:37.","DSpace SAF Submission Ingestion Package generated from Vireo submission #15638 on 2020-10-02 at 15:13:55"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/108501"],"dc:language":["en"],"dc:rights":["Copyright 2020 Ritwika Ghosh"],"dc:subject":["Programming Languages","Robotics","Distributed Systems","Formal Methods","Verification"],"dc:title":["Separation of distributed coordination and control for programming reliable robotics"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:48Z"}