Formal proofs of safe operating limits at wastewater resource recovery facilities

Our Motivation:

"Automated control strategies have the potential to reduce costs and emissions at wastewater resource recovery facilities (WRRFs), but ensuring the safety of commands is essential to adoption. We propose to extend formal methods for cyber-physical systems to the wastewater treatment domain by developing verification processes that enhance the safety of state-of-the-art control strategies."

Research Contribution

A preliminary framework for formal verification of WRRF control systems and translation of formal methods to the wastewater sector. Specifically, the framework will accept a SCADA set point for an existing cyber-physical system and conduct a formal proof that verifies the safety of that set point over a pre-defined time horizon (e.g., 24 hours) given assumptions such as design flow rates and regulatory limits.

Problem

Solution

Combine formal methods from computer science and process modeling from environmental engineering to create a formal verification tool that proves WRRF commands are safe under the facility-defined assumptions.

Added Value For The Industry

Streamlined deployment of automated controls in water and wastewater sectors through a verification tool for third-party communication.

Cooperation Partner

 Timeline

Contact Person

If you want to participate in the project please reach out to Fletcher Chapin.