Koord: A Language for Programming and Verifying Distributed Robotics Application
summary
Koord provides a high-level language that separates distributed coordination from platform-dependent control, with Controller Ports for sensing, planning and actuation and Distributed Shared Memory for communication. The system compiles and deploys to real platforms — compiles to real drones and racecar — and uses formal semantics in the K framework. Verification splits program turns (symbolic execution) from environment turns (DryVR black-box reachability), and DryVR shows drones stay bounded while the car can overshoot on a right turn.
AI-written summary · about
chapters (15)
- 0:00Intro
- 0:39Wide Applications of Multi-Robot Systems
- 1:19Building Reliable Distributed Robotic Systems
- 2:56Example: Delivery Application
- 3:42High Level Flowchart
- 4:57Building blocks or "Abstractions"
- 6:28Delivery Application in Koord
- 7:25Deploy and Simulate Delivery Application This video is sped up by 3x
- 7:59Case Study: Shape Formation
- 8:43Case Study: Distributed Mapping
- 9:22System and Robot Configurations
- 10:26Execution and Invariant
- 12:04Reason with Environment Turn
- 12:54Reachable Configurations in Environment Turns
- 13:52Conclusions
related talks
29mSynchronous Programming and Refinement Types in Robotics: From Verification to Implementation
18mRobotics in Polkadot
36mKlor: Choreographic Programming in Clojure
25mBuilding a PaaS for Robotics with Kubernetes
17mRapidly Build Distributed Applications using Orchestration
27mdora-rs: Modern Dataflow for Robotics
01h 30mImplementing, verifying and debugging distributed event-based systems
50mCadre: Building Reliable Distributed Stateful Applications