CSL Professor Sayan Mitra (ECE) and CS Professor Mahesh Viswanathan were recently awarded $500,000 from the National Science Foundation to support a grant entitled “From Simulations to Proofs for Cyberphysical Systems” that will seek additional ways to verify such systems in conjunction with simulations.
Written by Katie Carr, CSL
Because of the widespread presence of embedded controllers in vehicles, medical devices, and water, power and gas supply systems, there is an urgent need for efficient and accurate ways to ensure those systems’ reliability. Such systems are usually tested via simulations, but simulation can overlook defects. CSL Professor Sayan Mitra (ECE) and CS Professor Mahesh Viswanathan were recently awarded $500,000 from the National Science Foundation to support a grant entitled “From Simulations to Proofs for Cyberphysical Systems” that will seek additional ways to verify such systems in conjunction with simulations.
Sayan Mitra
Sayan Mitra
“Simulation, while being scalable and efficient, is incomplete,” said Sridhar Duggirala, a graduate student working on the project. “Verification, on the other hand, is computationally difficult and does not scale to large systems, but can provide mathematical guarantees.”
The group will be looking at developing scalable verification algorithms that combine simulations with system analysis or model parameters to rigorously establish properties of programs and systems. The goal is to develop efficient techniques, based on simulations, to determine the correctness of a system by observing many finite executions from different initial states. The goal is to develop an approach that would enable the analysis of a large network of systems.
“In our approach, we do several simulations around a number of critical scenarios and then we establish that any other, possibly infinitely many, unseen scenarios are covered as a combination of those critical ones,” Duggirala said. “And because we’ve analyzed those critical behaviors, we are able to show that all possible scenarios are safe.”
Duggirala added that the process allows researchers to extend the simulation verification technique to non-linear systems, as well as complex hybrid systems.
“This research could make formal verification of hybrid systems practical and this could be an enabling technology for automotive, aerospace and medical device industries,” Mitra said.