Formal Verification of Hardware Components in Critical Systems
Joint Authors
Solami, Eesa Al
Khan, Farrukh Aslam
Khan, Wilayat
Kamran, Muhammad
Naqvi, Syed Rameez
Alghamdi, Ahmed S.
Source
Wireless Communications and Mobile Computing
Issue
Vol. 2020, Issue 2020 (31 Dec. 2020), pp.1-15, 15 p.
Publisher
Hindawi Publishing Corporation
Publication Date
2020-02-20
Country of Publication
Egypt
No. of Pages
15
Main Subjects
Information Technology and Computer Science
Abstract EN
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’ 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 principle of duality 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.
American Psychological Association (APA)
Khan, Wilayat& Kamran, Muhammad& Naqvi, Syed Rameez& Khan, Farrukh Aslam& Alghamdi, Ahmed S.& Solami, Eesa Al. 2020. Formal Verification of Hardware Components in Critical Systems. Wireless Communications and Mobile Computing،Vol. 2020, no. 2020, pp.1-15.
https://search.emarefa.net/detail/BIM-1214511
Modern Language Association (MLA)
Khan, Wilayat…[et al.]. Formal Verification of Hardware Components in Critical Systems. Wireless Communications and Mobile Computing No. 2020 (2020), pp.1-15.
https://search.emarefa.net/detail/BIM-1214511
American Medical Association (AMA)
Khan, Wilayat& Kamran, Muhammad& Naqvi, Syed Rameez& Khan, Farrukh Aslam& Alghamdi, Ahmed S.& Solami, Eesa Al. Formal Verification of Hardware Components in Critical Systems. Wireless Communications and Mobile Computing. 2020. Vol. 2020, no. 2020, pp.1-15.
https://search.emarefa.net/detail/BIM-1214511
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references
Record ID
BIM-1214511