Process Quality Assessment in automatic management of wastewater treatment plants using Formal Verification

The well-known criteria for on-line monitoring of biological processes (nitrification and denitrification) in a Sequencing Batch Reactor (SBR) for municipal wastewater treatment, are based on the analysis of acquired online signals such as pH, oxido-reduction potential (ORP) and dissolved oxygen (DO) and are defined in a qualitative manner. An algorithm using neural networks is used to extract the relevant qualitative features from the signals such as “apexes” and “knees”. Once recognized, each feature is considered an event during the corresponding cycle: the completeness and correctness of the process depends on the sequence of events identified, with respect to the expected one. This is expressed by a direct translation into formal rules of the conditions known to the plant operators. These rules, serving as filters and classifiers, are checked using tools commonly applied for the Verification of Business Processes, of which the phases of a SBR cycle can be considered particular cases.