Formal Analysis of 2D Image Processing Filters using Theorem Proving

Abstract

Two-dimensional (2D) image processing systems are concerned with the processing of images represented as 2D arrays, and are widely used in medicine, transportation, and many other autonomous systems. The dynamics of these systems are generally modeled using 2D difference equations, which are mathematically analyzed using the 2D z-transform — a transformation of the difference-equation-based models into their corresponding algebraic equations, mapping the 2D arrays (2D discrete-time signals) over the (z₁, z₂)-domain. These (z₁, z₂)-domain representations are then used to analyze properties such as the transfer function and stability.

In this project, we use higher-order-logic (HOL) theorem proving to formally analyze image-processing filters. We formalize the 2D z-transform based on the multivariate theories of calculus using the HOL Light theorem prover, and formally analyze a generic (L₁, L₂)-order 2D infinite-impulse-response image-processing filter. We illustrate the practical effectiveness of the approach by formally analyzing a real-world second-order image-processing filter.

People