{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T15:15:26Z","timestamp":1773414926030,"version":"3.50.1"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2022,6,27]],"date-time":"2022-06-27T00:00:00Z","timestamp":1656288000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,6,27]],"date-time":"2022-06-27T00:00:00Z","timestamp":1656288000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100004482","name":"Kuwait University","doi-asserted-by":"publisher","award":["EO 07\/19"],"award-info":[{"award-number":["EO 07\/19"]}],"id":[{"id":"10.13039\/501100004482","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["EURASIP J. Adv. Signal Process."],"published-print":{"date-parts":[[2022,12]]},"abstract":"Abstract<\/jats:title>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<\/jats:italic>-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 ($$z_1$$<\/jats:tex-math>\n \n z<\/mml:mi>\n 1<\/mml:mn>\n <\/mml:msub>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>,$$z_2$$<\/jats:tex-math>\n \n z<\/mml:mi>\n 2<\/mml:mn>\n <\/mml:msub>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>)-domain. Finally, these ($$z_1$$<\/jats:tex-math>\n \n z<\/mml:mi>\n 1<\/mml:mn>\n <\/mml:msub>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>,$$z_2$$<\/jats:tex-math>\n \n z<\/mml:mi>\n 2<\/mml:mn>\n <\/mml:msub>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>)-domain representations are used to analyze various properties of these systems, such as transfer function and stability. Conventional techniques, such as paper-and-pencil proof methods, and computer-based simulation techniques for analyzing these filters cannot assert the accuracy of the analysis due to their inherent limitations like human error proneness, limited computational resources and approximations of the mathematical expressions and results. In this paper, as a complimentary technique, we propose to use formal methods, higher-order logic (HOL) theorem proving, for formally analyzing the image processing filters. These methods can overcome the limitations of the conventional techniques and thus ascertain the accuracy of the analysis. In particular, we formalize the 2D z<\/jats:italic>-transform based on the multivariate theories of calculus using the \u00a0theorem prover. Moreover, we formally analyze a generic ($$L_1,L_2$$<\/jats:tex-math>\n \n \n L<\/mml:mi>\n 1<\/mml:mn>\n <\/mml:msub>\n ,<\/mml:mo>\n \n L<\/mml:mi>\n 2<\/mml:mn>\n <\/mml:msub>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>)-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.<\/jats:p>","DOI":"10.1186\/s13634-022-00882-3","type":"journal-article","created":{"date-parts":[[2022,6,27]],"date-time":"2022-06-27T09:03:12Z","timestamp":1656320592000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formal analysis of 2D image processing filters using higher-order logic theorem proving"],"prefix":"10.1186","volume":"2022","author":[{"given":"Adnan","family":"Rashid","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1849-9316","authenticated-orcid":false,"given":"Sa\u2019ed","family":"Abed","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,6,27]]},"reference":[{"key":"882_CR1","volume-title":"Two-Dimensional Signal and Image Processing","author":"JS Lim","year":"1990","unstructured":"J.S. Lim, Two-Dimensional Signal and Image Processing (Prentice Hall, Englewood Cliffs, 1990)"},{"key":"882_CR2","volume-title":"Multidimensional Signal, Image, and Video Processing and Coding","author":"JW Woods","year":"2006","unstructured":"J.W. Woods, Multidimensional Signal, Image, and Video Processing and Coding (Elsevier, Amsterdam, 2006)"},{"issue":"2","key":"882_CR3","doi-asserted-by":"publisher","first-page":"1275","DOI":"10.1109\/COMST.2018.2869360","volume":"21","author":"R Hussain","year":"2018","unstructured":"R. Hussain, S. Zeadally, Autonomous cars: research results, issues, and future challenges. IEEE Commun. Surv. Tutor. 21(2), 1275\u20131313 (2018)","journal-title":"IEEE Commun. Surv. Tutor."},{"issue":"5","key":"882_CR4","first-page":"161","volume":"2018","author":"H Blasinski","year":"2018","unstructured":"H. Blasinski, J. Farrell, T. Lian, Z. Liu, B. Wandell, Optimizing image acquisition systems for autonomous driving. Electron. Imaging 2018(5), 161\u20131 (2018)","journal-title":"Electron. Imaging"},{"issue":"suppl\u20132","key":"882_CR5","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1259\/bjr\/17464219","volume":"77","author":"C Behrenbruch","year":"2004","unstructured":"C. Behrenbruch, S. Petroudi, S. Bond, J. Declerck, F. Leong, J. Brady, Image filtering techniques for medical image post-processing: an overview. Br. J. Radiol. 77(suppl\u20132), 126\u2013132 (2004)","journal-title":"Br. J. Radiol."},{"key":"882_CR6","doi-asserted-by":"crossref","unstructured":"G. Hemalatha, C. Sumathi, Preprocessing techniques of facial image with median and Gabor filters, in: Information Communication and Embedded Systems (IEEE, 2016), pp. 1\u20136","DOI":"10.1109\/ICICES.2016.7518860"},{"key":"882_CR7","doi-asserted-by":"crossref","unstructured":"A.J. Dur\u00e1n, M. P\u00e9rez, J.L. Varona, The Misfortunes of a Mathematicians\u2019 Trio using Computer Algebra Systems: Can We Trust? CoRR. arXiv:1312.3270 (2013)","DOI":"10.1090\/noti1173"},{"key":"882_CR8","first-page":"7162","volume-title":"Formal Verification Methods. Encyclopedia of Information Science and Technology","author":"O Hasan","year":"2015","unstructured":"O. Hasan, S. Tahar, Formal Verification Methods. Encyclopedia of Information Science and Technology (IGI Global Pub, Hershey, 2015), pp. 7162\u20137170"},{"key":"882_CR9","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511576430","volume-title":"Handbook of Practical Logic and Automated Reasoning","author":"J Harrison","year":"2009","unstructured":"J. Harrison, Handbook of Practical Logic and Automated Reasoning (Cambridge University Press, Cambridge, 2009)"},{"key":"882_CR10","doi-asserted-by":"crossref","unstructured":"M.J. Gordon, HOL: a proof generating system for higher-order logic, in VLSI Specification, Verification and Synthesis. SECS, vol. 35 (Springer, Berlin, 1988), pp. 73\u2013128","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"882_CR11","doi-asserted-by":"crossref","unstructured":"J. Harrison, HOL light: a tutorial introduction, in Formal Methods in Computer-Aided Design. LNCS, vol. 1166 (Springer, 1996), pp. 265\u2013269","DOI":"10.1007\/BFb0031814"},{"key":"882_CR12","doi-asserted-by":"crossref","unstructured":"J. Harrison, HOL light: a tutorial introduction, in Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201996). Lecture Notes in Computer Science, vol. 1166, ed. by M. Srivas, A. Camilleri (Springer, Berlin, 1996), pp. 265\u2013269","DOI":"10.1007\/BFb0031814"},{"key":"882_CR13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511811326","volume-title":"ML for the Working Programmer","author":"L Paulson","year":"1996","unstructured":"L. Paulson, ML for the Working Programmer (Cambridge University Press, Cambridge, 1996)"},{"key":"882_CR14","doi-asserted-by":"crossref","unstructured":"U. Siddique, M.Y. Mahmoud, S. Tahar, On the formalization of z-transform in HOL, in Interactive Theorem Proving (Springer, 2014), pp. 483\u2013498","DOI":"10.1007\/978-3-319-08970-6_31"},{"key":"882_CR15","doi-asserted-by":"crossref","unstructured":"S.H. Taqdees, O. Hasan, Formalization of laplace transform using the multivariable calculus theory of HOL light, in Logic for Programming Artificial Intelligence and Reasoning(Springer, 2013), pp. 744\u2013758","DOI":"10.1007\/978-3-642-45221-5_50"},{"key":"882_CR16","volume-title":"Multidimensional Digital Signal Processing","author":"DE Dudgeon","year":"1983","unstructured":"D.E. Dudgeon, Multidimensional Digital Signal Processing (Prentice Hall, Engewood Cliffs, 1983)"}],"container-title":["EURASIP Journal on Advances in Signal Processing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s13634-022-00882-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1186\/s13634-022-00882-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s13634-022-00882-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,27]],"date-time":"2022-06-27T09:24:41Z","timestamp":1656321881000},"score":1,"resource":{"primary":{"URL":"https:\/\/asp-eurasipjournals.springeropen.com\/articles\/10.1186\/s13634-022-00882-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,27]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["882"],"URL":"https:\/\/doi.org\/10.1186\/s13634-022-00882-3","relation":{},"ISSN":["1687-6180"],"issn-type":[{"value":"1687-6180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,6,27]]},"assertion":[{"value":"3 November 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 June 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 June 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"All procedures performed in this paper were in accordance with the ethical standards of research community.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethics approval and consent to participate"}},{"value":"Not applicable.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent for publication"}},{"value":"The authors declare that they have no competing interests.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"53"}}