CSL researchers work to guarantee system reliability

It is said that the only guarantees in life are death and taxes. CSL graduate student Chuchu Fan and adviser Sayan Mitra are working to add power systems to that list in their Siebel Energy Institute-funded project, “A Formal Verification and Synthesis Tool for Safety 

Critical Power Grid Infrastructures and Cyber-physical Systems."

“We take reliability of power systems for granted and rarely think about their failures,” said Fan, a student in electrical and computer engineering. “As these systems become more automated and software-intensive, they are also becoming vulnerable to bugs and attacks. We are grateful to receive this opportunity to investigate the role of formal verification in the analysis of power systems.”

Fan and Mitra are expanding their previous research and applying it to power systems. Their previous research looked at formal verification of complex autonomous vehicle scenarios, such as a spacecraft maneuvering to dock with another spacecraft and a self-driving car overtaking and merging around other cars. These scenarios have clear safety requirements like maintaining separation and speed. Figuring out the specific goals for the power systems being used will be one of the initial goals of this project.

“We need to learn more about specifications that power system researchers care about,” said Fan. “This is a very challenging problem because power systems have different requirement across different spatial and temporal scales. We need to take a fresh look at our specification approach to fit into this domain.”

Rather than specifications that limit speed, a power system, like an electric grid, may need a rule that maintains stability or integrity during an energy shortage. The team plans to develop a tool that can verify the behavior of the systems, thereby recognizing any disturbances or uncertainties. Once the dangerous behavior is quantified, algorithms can be developed to prevent this type of behavior in the future.

The technology developed in this research has the potential for applications beyond power distribution in other types of networked systems.

“Testing is important, but putting all your eggs in the testing basket may not be the smartest way to get a high-level of assurance,” said Mitra. “There are currently no scalable methods for formal verification that take 

advantage of the inherent structures in networked systems like symmetries and repeated sub-structures.”

Using the aforementioned structures, Mitra and Fan are expecting to chart a new research direction for verification of systems.

This research was funded for two years by the Siebel Energy Institute at $50,000. Two other CSL researchers, William Sanders and Max Liu, were awarded these grants as well. Sanders for his proposal "The Design and Implementation of a Distributed Denial of Service-Tolerant Network Architecture for the Future CPS Cloud” and Liu for "Secure Cloud-Based Applications for Enhancing Power Grid Resilience." Eleven grants were awarded in total, with the University of Illinois at Urbana-Champaign receiving the most out of any institution.