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.
CSL Assistant Professor Sayan Mitra is addressing that problem 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.
“For software that interacts with physical processes, we can exploit properties like continuity and stability to analyze the complete cyber systems,” said Mitra, a member of Illinois’ electrical and computer engineering faculty. “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 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.”
