StarL: Towards a unified framework for programming, simulating and verifying distributed robotic systems

Yixiao Lin, Sayan Mitra

Research output: Contribution to journalArticlepeer-review


We developed StarL as a framework for programming, simulating, and verifying distributed systems that interacts with physical processes. StarL framework has (a) a collection of distributed primitives for coordination, such as mutual exclusion, registration and geocast that can be used to build sophisticated applications, (b) theory libraries for verifying StarL applications in the PVS theorem prover, and (c) an execution environment that can be used to deploy the applications on hardware or to execute them in a discrete event simulator. The primitives have (i) abstract, nondeterministic specifications in terms of invariants, and assume-guarantee style progress properties, (ii) implementations in Java/Android that always satisfy the invariants and attempt progress using best effort strategies. The PVS theories specify the invariant and progress properties of the primitives, and have to be appropriately instantiated and composed with the application's state machine to prove properties about the application. We have built two execution environments: one for deploying applications on Android/iRobot Create platform and a second one for simulating large instantiations of the applications in a discrete even simulator. The capabilities are illustrated with a StarL application for vehicle to vehicle coordination in an automatic intersection that uses primitives for point-topoint motion, mutual exclusion, and registration.

Original languageEnglish (US)
Article numbera9
Pages (from-to)83-92
Number of pages10
JournalACM SIGPLAN Notices
Issue number5
StatePublished - May 2015


  • Distributed systems
  • Mechanical theorem proving
  • Programming models
  • Robotics
  • Verification

ASJC Scopus subject areas

  • Computer Science(all)


Dive into the research topics of 'StarL: Towards a unified framework for programming, simulating and verifying distributed robotic systems'. Together they form a unique fingerprint.

Cite this