Waqar Ahmad

National University of Sciences and Technology

Author Statistics

Papers

Citation

H-Index

i-10 index

Research Trends

Author Order

Document Type

Co-Authors

Osman Hasan

National University of Sciences and Technology

Sofiène Tahar

Concordia University

Mohamed Abdelghany

Concordia University

Yassmeen Elderhalli

Concordia University

Mohamed Salah Hamdi

University of Carthage

Haaris Rasool

Vrije Universiteit Brussel

Sowmith Nethula

Concordia University

Aazim Rasool

North China Electric Power University

Usman Pervez

National University of Sciences and Technology

Tahir Ayub

Cooperative Institutions

National University of Sciences and Technology

Concordia University

University of the Sciences

United Arab Emirates University

National University of Computer and Emerging Sciences

North China Electric Power University

Polytechnique Montréal

Tennessee Technological University

Information Technology University

University of Engineering and Technology Taxila

Author Statistics

Papers

Citation

H-Index

i-10 index

Research Field

Formal Dependability Analysis using Higher-order-logic Theorem Proving

Waqar Ahmad

Source

Cite

Citations (7)

A Hybrid Model Checking and Theorem Proving based Approach for Fault Tree Analysis

Shahid Khan Waqar Ahmad Osman Hasan

Static fault trees (SFT)s are used for conducting dependability analysis and thus are extensively utilized in various functional safety standards defined by the IEC and ISO for automotive applications. Traditionally, SFTs are manually developed by domain experts through a very cumbersome and error prone process. Once the SFT is available, quantitative fault tree analysis (FTA) is carried out using analytical approaches, e.g., probabilistic model checking and theorem proving. While the former is limited to exponential distributions, the latter can analyze fault trees (FT)s with arbitrary probability distributions. This paper proposes to combine model checking-based automatic FT generation and theorem proving based FTA to ensure a more rigorous and complete approach for FTA. The proposed approach particularly utilizes 1) the xSAP safety assessment platform to automatically generate SFTs from a functionally verified system model and 2) the HOL4 theorem prover to analyze the xSAP-generated SFTs. The usefulness of the approach is illustrated using the case study of an automated vehicle system.

10.1109/smacd55068.2022.9816211

Cite

Citations (0)

Formal Probabilistic Analysis of Dynamic Fault Trees in HOL4.

arXiv (Cornell University) (2018)

Yassmeen Elderhalli Waqar Ahmad Osman Hasan Sofiène Tahar

Dynamic Fault Trees (DFTs) is a widely used failure modeling technique that allows capturing the dynamic failure characteristics of systems in a very effective manner. Simulation and model checking have been traditionally used for the probabilistic analysis of DFTs. Simulation is usually based on sampling and thus its results are not guaranteed to be complete, whereas model checking employs computer arithmetic and numerical algorithms to compute the exact values of probabilities, which contain many round-off errors. Leveraging upon the expressive and sound nature of higher-order-logic (HOL) theorem proving, we propose, in this work, a formalization of DFT gates and their probabilistic behavior as well as some of their simplification properties in HOL. This formalization would allow us to conduct the probabilistic analysis of DFTs by verifying generic mathematical expressions about their behavior in HOL. In particular, we formalize the AND, OR, Priority-AND, Functional DEPendency, Hot SPare, Cold SPare and the Warm SPare gates and also verify their corresponding probabilistic expressions in HOL. Moreover, we formally verify an important property, Pr(X

HOL

Spare part

Probabilistic CTL

Source

Cite

Citations (0)

Formal Reliability Analysis of an Integrated Power Generation System Using Theorem Proving

IEEE Systems Journal (2020)

Waqar Ahmad Osman Hasan Falah Awwad Nabil Bastaki Syed Rafay Hasan

In recent years, alongside conventional generators, the renewable energy-based power systems consisting of wind and solar farms, and the batteries with large capacities, termed as energy storage systems (ESS), have been increasingly installed and operated for electric power generation. The uncertainties in the generated power, due to the variability of wind speed or solar radiation and the improper charging and discharging of the batteries, greatly affects the proper operation as well as the reliability of these power systems. Due to their huge cost and safety-critical nature, the reliability analysis using traditional simulation tools, which are mainly based on Monte Carlo approach, may not be an appropriate choice. In this article, we propose to use higher order logic theorem proving to conduct an accurate reliability analysis of the power systems consisting of conventional generators, the renewable energy sources, and the ESS. For this purpose, we formally verify the generic convolution properties for n-discrete random variables and also formalize the properties of Binomial random variables in the context of power system. For illustration purposes, we present the reliability analysis of IEEE 118-bus test system consisting of 11 conventional generators, 1 wind/solar farm of 5 identical units, and 4 identical ESS batteries.

10.1109/jsyst.2020.2970107

Cite

Citations (5)

Reliability modeling and analysis of communication networks

Journal of Network and Computer Applications (2016)

Waqar Ahmad Osman Hasan Usman Pervez Junaid Qadir

10.1016/j.jnca.2016.11.008

Cite

Citations (98)

MPPT based ASBC controller and solar panel monitoring system

Haaris Rasool Abdul Mutal Aazim Rasool Waqar Ahmad Ataul Aziz Ikram

The simulation work presented in this paper was carried out on microcontroller based Automated Solar Battery Charge Controller (ASBCC) for controlling the overcharging and deep discharging of a battery. The purpose of ASBCC is switching with help of programmed controller. Battery Charge Circuit (BCC) regulates the solar power to charge the battery to maximum specific level. Equipment's monitoring has always been essential. Software based Graphical User Interface (GUI) shows the digital values of output voltage, current, temperature and power of solar panel and battery charged status. These data is stored into the computer data base. GUI also indicates battery charging, discharging and load connected to panel. Maximum Power Point Tracking (MPPT) is used to extract the maximum power from Solar panel and force the panel to operate at required power.

Charge controller

Maximum power principle

Graphical user interface

10.1109/icesp.2014.7347002

Cite

Citations (10)

Formal Verification of ECCs for Memories Using ACL2

Journal of Electronic Testing (2020)

Mahum Naseer Waqar Ahmad Osman Hasan

Hamming distance

Code (set theory)

10.1007/s10836-020-05904-2