skip to main content

Illinois researchers accelerate autonomous tech development


Sayan Mitra, Sasa Misailovic, Lizzie Roehrs

Autonomous systems are poised to transform transportation, manufacturing, entertainment, and agriculture; however, developing reliable autonomous systems requires a building full of engineers. Doing so requires a very different level of effort than creating comparable mobile apps. CSL Professor Sayan Mitra and CS Assistant Professor Sasa Misailovic are exploring new programming languages and tools that aim to make it easier to build autonomous systems and therefore broaden participation in that enterprise.

Drones flying in robotics labDrones delivering in a warehouse environmentKoord delivery applicationSimulation of Koord formation

“The core of any programming system is the ‘abstractions’ -- the building blocks of code or functions that can be used by programmers to build larger functions, libraries, applications, and systems,” says Mitra, an Electrical and Computer Engineering professor. “The abstractions of a language define the mindset, the units of thought, the core concepts.”

Mitra says an example of this is the x86 assembly language or instruction set that defines the operations can be performed on data and how data can be moved between the CPU and the memory. This makes it possible to run the same application program, such as the popular game ‘Among Us’, on different computers, even from different manufacturers (Apple and Android).

“For robotics and autonomous systems, we do not yet have good abstractions. Impressive applications are developed, but they are hyper-targeted for a specific hardware platform,” says Misailovic. “This not only makes it difficult to port applications, it also complicates debugging and verification.”

In their recent paper published in OOPSLA 2020, Mitra and Misailovic and their graduate students Ritwika Ghosh and Chiao Hsieh, have proposed a new programming language called “Koord for distributed robotics” that provides abstractions for control and coordination that addresses some of these issues. For example, Koord, a formation flight application -- like the ones used for drone shows -- can be written in just 10 lines of Koord code. This code can then be deployed on actual drones or simulated.

There are several other applications discussed in the paper. A distributed delivery application is only about 40 lines and has shown how the same application can be compiled and ported to quadcopters and ground vehicles. Koord is a part of the CyPhyHouse (a toolchain that aims to provide similar programming, debugging, and deployment benefits for distributed mobile robotic applications) project which is led by Mitra and Geir Dullerud of CSL.

“One of the key challenges for safety and reliability in autonomous systems is coping with uncertainty,” says Mitra. “In the new NSF project, we focus on three important forms of uncertainty: Noisy data from sensors and perception modules, asynchrony of distributed computation, and heuristic computation of the software that makes decisions.”

These sources bring various challenges for developing and validating software modules of autonomous systems. To address these challenges, they propose a language-based framework for analysis of programs for autonomous systems that treats quantification and management of uncertainty as first-class-citizens.

“Our main insight is to combine logic-based verification techniques with probabilistic program analysis,” says Misailovic. “Previously, my students and I have worked on languages and verification techniques for probabilistic distributed systems and computer networks. Our goal in this project is to integrate these techniques with emerging approaches for statistical model checking to answer complex verification queries in an automated fashion.”

Mitra and Misailovic plan to evaluate their techniques on real robots, in CyPhyHouse, and also the GEM autonomous vehicle platform. This combination of principled reasoning techniques and real-world evaluation will help them build the first end-to-end reasoning framework that can inform not only verification and inference, but also data collection for refining further verification and/or user’s complex programs.

This framework will help them educate students and researchers in programming languages, formal methods, and cyber-physical systems through new course materials and tutorials on its demonstrated results.