Abstract

Two-dimensional (2D) image processing systems are concerned with the processing of the 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. It mainly involves a transformation of the difference equations-based models of these systems to their corresponding algebraic equations, mapping the 2D arrays (2D discrete-time signals) over the (z1,z2)-domain. Finally, these (z1,z2)-domain representations are used to analyze various properties of these systems, such as transfer function and stability. In this project, we propose to use formal methods, higher-order logic (HOL) theorem proving, for formally analyzing the image processing filters. In particular, we formalize the 2D z-transform based on the multivariate theories of calculus using the HOL Light theorem prover. Moreover, we formally analyze a generic (L1,L2)-order 2D infinite impulse response image processing filter. We illustrate the practical effectiveness of our proposed approach by formally analyzing a second-order image processing filter.

Framework

People

• Adnan Rashid, SEECS, NUST, Pakistan
• Osman Hasan, SEECS, NUST, Pakistan
• Sa'ed Abed, Kuwait University, Kuwait

Publications

1. A. Rashid, Sa'ed Abed and O. Hasan, “Formal Stability Analysis of Two-dimensional Digital Image Processing Filters”, International Congress on Information and Communication Technology (ICICT), Lecture Notes in Networks and Systems (LNNS), Springer, Vol. 693, pp: 583-591, London, UK, 2023.
2. A. Rashid, Sa'ed Abed and O. Hasan, “Formal Analysis of 2D Image Processing Filters using Higher-order-logic Theorem Proving”, EURASIP Journal on Advances in Signal Processing, Springer, No. 53, pp. 1-18, DOI:10.1186/s13634-022-00882-3, 2022.