{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,11]],"date-time":"2025-04-11T11:08:41Z","timestamp":1744369721749,"version":"3.37.3"},"reference-count":38,"publisher":"Wiley","license":[{"start":{"date-parts":[[2020,2,20]],"date-time":"2020-02-20T00:00:00Z","timestamp":1582156800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100011665","name":"Deanship of Scientific Research, King Saud University","doi-asserted-by":"publisher","award":["RGP-214"],"award-info":[{"award-number":["RGP-214"]}],"id":[{"id":"10.13039\/501100011665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Wireless Communications and Mobile Computing"],"published-print":{"date-parts":[[2020,2,20]]},"abstract":"<jats:p>Hardware components, such as memory and arithmetic units, are integral part of every computer-controlled system, for example, Unmanned Aerial Vehicles (UAVs). The fundamental requirement of these hardware components is that they must behave as desired; otherwise, the whole system built upon them may fail. To determine whether or not a component is behaving adequately, the desired behaviour of the component is often specified in the Boolean algebra. Boolean algebra is one of the most widely used mathematical tools to analyse hardware components represented at gate level using Boolean functions. To ensure reliable computer-controlled system design, simulation and testing methods are commonly used to detect faults; however, such methods do not ensure absence of faults. In critical systems\u2019 design, such as UAVs, the simulation-based techniques are often augmented with mathematical tools and techniques to prove stronger properties, for example, absence of faults, in the early stages of the system design. In this paper, we define a lightweight mathematical framework in computer-based theorem prover Coq for describing and reasoning about Boolean algebra and hardware components (logic circuits) modelled as Boolean functions. To demonstrate the usefulness of the framework, we (1) define and prove the correctness of <jats:italic>principle of duality<\/jats:italic> mechanically using a computer tool and all basic theorems of Boolean algebra, (2) formally define the algebraic manipulation (step-by-step procedure of proving functional equivalence of functions) used in Boolean function simplification, and (3) verify functional correctness and reliability properties of two hardware components. The major advantage of using mechanical theorem provers is that the correctness of all definitions and proofs can be checked mechanically using the type checker and proof checker facilities of the proof assistant Coq.<\/jats:p>","DOI":"10.1155\/2020\/7346763","type":"journal-article","created":{"date-parts":[[2020,2,20]],"date-time":"2020-02-20T23:36:53Z","timestamp":1582241813000},"page":"1-15","source":"Crossref","is-referenced-by-count":7,"title":["Formal Verification of Hardware Components in Critical Systems"],"prefix":"10.1155","volume":"2020","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0993-5964","authenticated-orcid":true,"given":"Wilayat","family":"Khan","sequence":"first","affiliation":[{"name":"Department of Electrical and Computer Engineering, COMSATS University Islamabad, Wah Campus, Pakistan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6639-5688","authenticated-orcid":true,"given":"Muhammad","family":"Kamran","sequence":"additional","affiliation":[{"name":"Department of Cyber Security, College of Computer Science and Engineering, University of Jeddah, Jeddah, Saudi Arabia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6954-926X","authenticated-orcid":true,"given":"Syed Rameez","family":"Naqvi","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, COMSATS University Islamabad, Wah Campus, Pakistan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7023-7172","authenticated-orcid":true,"given":"Farrukh Aslam","family":"Khan","sequence":"additional","affiliation":[{"name":"Center of Excellence in Information Assurance (CoEIA), King Saud University, Riyadh, Saudi Arabia"}]},{"given":"Ahmed S.","family":"Alghamdi","sequence":"additional","affiliation":[{"name":"Department of Cyber Security, College of Computer Science and Engineering, University of Jeddah, Jeddah, Saudi Arabia"}]},{"given":"Eesa","family":"Alsolami","sequence":"additional","affiliation":[{"name":"Department of Cyber Security, College of Computer Science and Engineering, University of Jeddah, Jeddah, Saudi Arabia"}]}],"member":"311","reference":[{"key":"1","doi-asserted-by":"publisher","DOI":"10.1002\/ett.3603"},{"key":"2","first-page":"1","volume":"78","year":"2018","journal-title":"Multimedia Tools and Applications"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1016\/j.comcom.2019.12.004"},{"year":"2019","key":"4"},{"issue":"8","key":"6","first-page":"30","volume":"23","year":"2012","journal-title":"GPS World"},{"year":"June 2019","key":"10"},{"key":"11","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1109\/2.58215","volume":"23","year":"1990","journal-title":"Computer"},{"first-page":"407","volume-title":"Formal methods in resilient systems design: application to multi-UAV system-of-systems control","year":"2018","key":"14"},{"key":"15","first-page":"28","volume":"42","year":"2013","journal-title":"Mobile and Wireless"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1155\/2014\/14859510.1155\/2014\/148595"},{"year":"1854","key":"19"},{"key":"20","doi-asserted-by":"crossref","first-page":"713","DOI":"10.1109\/EE.1938.6431064","volume":"57","year":"1938","journal-title":"Electrical Engineering"},{"key":"26","first-page":"593","volume":"72","year":"1953","journal-title":"Transactions of the American Institute of Electrical Engineers, Part I: Communication and Electronics"},{"key":"28","doi-asserted-by":"crossref","first-page":"1377","DOI":"10.1109\/TCAD.2002.804386","volume":"21","year":"2002","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"year":"2017","key":"29"},{"key":"34","first-page":"75","volume":"174","year":"2007","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"35","doi-asserted-by":"publisher","DOI":"10.3390\/electronics7060081"},{"year":"2018","key":"36"},{"first-page":"429","volume-title":"The state explosion problem","year":"1998","key":"37"},{"first-page":"1","volume-title":"Model checking and the state explosion problem","year":"2012","key":"38"},{"year":"2013","key":"39"},{"first-page":"15","volume-title":"An overview of formal methods tools and techniques","year":"2011","key":"41"},{"year":"2013","key":"43"},{"volume":"2283","year":"2002","key":"45"},{"year":"1998","key":"46"},{"key":"48","first-page":"274","volume":"35","year":"1933","journal-title":"Transactions of the American Mathematical Society"},{"key":"51","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/j.jal.2011.01.002","volume":"9","year":"2011","journal-title":"Journal of Applied Logic"},{"volume":"12","year":"2012","key":"57"},{"year":"1999","key":"58"},{"key":"59","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","year":"2003","journal-title":"Advances in Computers"},{"year":"2005","key":"62"},{"key":"63","doi-asserted-by":"publisher","DOI":"10.1109\/access.2019.2895261"},{"key":"64","doi-asserted-by":"publisher","DOI":"10.1186\/s13673-018-0144-7"},{"key":"65","doi-asserted-by":"publisher","DOI":"10.3233\/jcs-150529"},{"key":"66","doi-asserted-by":"publisher","DOI":"10.1109\/tc.1985.1676600"},{"key":"69","doi-asserted-by":"publisher","DOI":"10.1007\/s10617-019-09226-1"},{"key":"70","doi-asserted-by":"publisher","DOI":"10.4028\/www.scientific.net\/amm.892.134"},{"key":"72","doi-asserted-by":"publisher","DOI":"10.1109\/tifs.2011.2160627"}],"container-title":["Wireless Communications and Mobile Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/wcmc\/2020\/7346763.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/wcmc\/2020\/7346763.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/wcmc\/2020\/7346763.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T23:34:52Z","timestamp":1588808092000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.hindawi.com\/journals\/wcmc\/2020\/7346763\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,20]]},"references-count":38,"alternative-id":["7346763","7346763"],"URL":"https:\/\/doi.org\/10.1155\/2020\/7346763","relation":{},"ISSN":["1530-8669","1530-8677"],"issn-type":[{"type":"print","value":"1530-8669"},{"type":"electronic","value":"1530-8677"}],"subject":[],"published":{"date-parts":[[2020,2,20]]}}}