Final published version
Licence: CC BY-NC-ND: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License
Research output: Contribution to Journal/Magazine › Journal article › peer-review
Research output: Contribution to Journal/Magazine › Journal article › peer-review
}
TY - JOUR
T1 - FABI
T2 - A formal analyser of binary image objects identification tools
AU - Iqbal, Saima
AU - Altamimi, Ahmed B.
AU - Khan, Wilayat
AU - Alsaffar, Mohammad
AU - Ahmad, Aakash
AU - Alfaisal, Fahad F.
PY - 2024/12/31
Y1 - 2024/12/31
N2 - In computer vision, the goal of object identification in images is to track or count objects such as persons, cars, animals and so on. Object detection techniques have found their place in several applications such as video analytic, contact-less checkouts, inventory management, defect detection, productivity improvements, landscape patch analysis and many more. One of the most common techniques for image object identification in binary images is the four and eight-neighbourhood of pixels in the images. The image object identification mechanisms based on the four or eight-neighbour (more generally, the k nearest neighbours) techniques identify objects in the images but there is no guarantee of their correctness. To the best of our knowledge, there is no image object identification tool with proof that it correctly identifies the image objects. To meet the high standards of correctness, we provide a formal foundation to allow proof of correctness of the image object identification tools based on the four or eight-neighbourhood techniques. As a proof of concept, an object identification tool is developed by implementing both, the four neighbour and eight neighbour, techniques in a general purpose programming language. The tool is experimentally evaluated by running it against real life RGB images. Furthermore, the correctness of the objects identified by the prototype tool are checked by encoding the objects in the formal notations and running the predicate over each object using the type checker program of the Coq tool.
AB - In computer vision, the goal of object identification in images is to track or count objects such as persons, cars, animals and so on. Object detection techniques have found their place in several applications such as video analytic, contact-less checkouts, inventory management, defect detection, productivity improvements, landscape patch analysis and many more. One of the most common techniques for image object identification in binary images is the four and eight-neighbourhood of pixels in the images. The image object identification mechanisms based on the four or eight-neighbour (more generally, the k nearest neighbours) techniques identify objects in the images but there is no guarantee of their correctness. To the best of our knowledge, there is no image object identification tool with proof that it correctly identifies the image objects. To meet the high standards of correctness, we provide a formal foundation to allow proof of correctness of the image object identification tools based on the four or eight-neighbourhood techniques. As a proof of concept, an object identification tool is developed by implementing both, the four neighbour and eight neighbour, techniques in a general purpose programming language. The tool is experimentally evaluated by running it against real life RGB images. Furthermore, the correctness of the objects identified by the prototype tool are checked by encoding the objects in the formal notations and running the predicate over each object using the type checker program of the Coq tool.
U2 - 10.1109/access.2024.3414374
DO - 10.1109/access.2024.3414374
M3 - Journal article
VL - 12
SP - 186313
EP - 186325
JO - IEEE Access
JF - IEEE Access
SN - 2169-3536
ER -