ECE ILLINOIS Facebook ECE ILLINOIS on Twitter ECE ILLINOIS Alumni and Friends on LinkedIn ECE ILLINOIS Instagram

Contact Info

Brad Petersen
Director of
Communications
2052 ECE Building
306 N. Wright Street
Urbana, IL 61801
Phone: (217) 244-6376
bradp@illinois.edu

Contact Info

Meg Dickinson
Communications Specialist
2016 ECE Building
306 N. Wright Street
Urbana, IL 61801
Phone: (217) 300-6664
megd@illinois.edu

Subscribe to ECE ILLINOIS News

Recent News

New ECE class gives students an in-depth look at the engineering process

New ECE class gives students an in-depth look at the engineering process

Starting this semester, ECE ILLINOIS will offer students an opportunity to study the engineering design process and possibly get a head start on their Senior Design projects with a new class called ECE 398, Special Topics in ECE.

Mitra develops verification tool for trustworthy cyber-physical systems

 Subscribe to ECE ILLINOIS News

By Kim Gudeman, Coordinated Science Laboratory
July 11, 2014

  • Information systems are replacing humans in tasks from flying aircraft to regulating heartbeats. These systems need to be ensured as safe and reliable before being deployed, especially in fields where failure could be fatal.
  • ECE ILLINOIS Assistant Professor Sayan Mitra is working on a tool that uses novel algorithms to formally guarantee the safety of software.
  • Mitra's work was selected as one of three finalists for the Best Paper Award at the Conference on Hybrid Systems held in April in Berlin.

Over the past few decades, information systems have increasingly replaced human operators and processes, with technology assisting in everything from flying aircraft to regulating heartbeats. As the movement toward more autonomous systems continues, there is a growing need to ensure that these systems are safe and reliable before they are deployed – especially in fields where failure could be fatal.

ECE Assistant Professor Sayan Mitra is addressing that problem in research for the Coordinated Science Laboratory by designing a tool that provides formal guarantees for the safety and reliability of software, using novel algorithms that leverage the properties of physics and apply them to cyber systems.

Sayan  Mitra
Sayan Mitra

“For software that interacts with physical processes, we can exploit properties like continuity and stability to analyze the complete cyber systems,” Mitra said. “These properties of the physical world can guide exploration of how software behaves in different scenarios and how it can break.”

Software verification isn’t a new field of study, but traditional tests have proven largely incapable of testing for every possible outcome. While the tests can verify a finite number of outcomes in a laboratory setting, they have struggled to account for new behaviors that are introduced when systems are deployed in the real world.

Mitra’s tools overcome that problem by combining fast simulations with formal and mathematical analysis. His research team recently partnered with NASA to verify the correctness of software that would facilitate a parallel landing protocol enabling planes to approach the runway in closer formation than is currently allowed. For the new protocol to work, anti-collision software, which monitors other planes and alerts the cockpit if planes get too close, must be precise and reliable.

“The planes are moving continuously in space, and if you run a simulation using the physics of the planes, we can see how the approach would work with different wind velocities, plane speeds, etc.,” said Mitra, whose work in this area was presented at the 2014 International Symposium on Formal Methods, held in May in Singapore.

Mitra is applying the same technique to pacemakers. He is working to verify models of pacemakers and cardiac tissue created by researchers at Stony Brook (New York) University and Oxford University. The work employs a second research breakthrough made by Mitra’s team: Decomposing a large, complex system into small pieces in order to infer properties about the system. It is the first time that this type of decomposition has been used for simulation-based verification.

The verification tool proves that an alarm is raised before potential safety violations by computing future behavior of the physical aircraft as well as the alerting software.
The verification tool proves that an alarm is raised before potential safety violations by computing future behavior of the physical aircraft as well as the alerting software.

The work was selected as one of three finalists for the Best Paper Award at the Conference on Hybrid Systems held in April in Berlin.

In addition, the research has garnered attention for other members of the team. Graduate student Parasara Sridhar Duggirala, co-advised by Professor Mahesh Viswanathan and Mitra, recently won the Feng Chen Memorial Award in Software Engineering, bestowed by the Illinois Department of Computer Science. Duggirala also was selected to attend the Heidelberg Laureate Forum, in which the world’s top young scientists are invited to learn from Abel, Fields and Turing Laureates.

Mitra is exploring other avenues in which to apply his research, including autonomous cars.

“As we push to reduce workload for human operators and operating costs in general, we’ll see even more need for autonomy in systems,” Mitra said. “Our goal is to make sure they have a high level of trustworthiness."

Editor's note: media inquiries should be directed to Brad Petersen, Director of Communications, at bradp@illinois.edu or (217) 244-6376.

 Subscribe to ECE ILLINOIS News