arXiv subjects

Osman Hasan

Publications and source records attributed to Osman Hasan.

At least 37 records · Page 2Linked to original sources

arXiv2019

Formal Analysis of the Biological Circuits using Higher-order-logic Theorem Proving

Synthetic Biology is an interdisciplinary field that utilizes well-established engineering principles, ranging from electrical, control and computer systems, for analyzing the biological systems, such as biological circuits, enzymes, pathways and controllers. Traditionally, these biological systems, i.e., the genetic circuits are analyzed using paper-and-pencil proofs and computer-based simulations techniques. However, these methods cannot provide accurate results due to their inherent limitations such as human error-proneness, round-off errors and the unverified algorithms present in the core of the tools, providing such analyses. In this paper, we propose to use higher-order-logic theorem proving as a complementary technique for analyzing these systems and thus overcome the above-mentioned issues. In particular, we propose a higher-order-logic theorem proving based framework to formally reason about the genetic circuits used in synthetic biology. The main idea is to, first, model the continuous dynamics of the genetic circuits using differential equations. The next step is to obtain the systems' transfer function from their corresponding block diagram representations. Finally, the transfer function based analysis of these differential equation based models is performed using the Laplace transform. To illustrate the practical utilization of our proposed framework, we formally analyze the genetic circuits of activated and repressed expressions of protein.

cs.LO↗

arXiv2019

Dynamic Dependability Analysis of Shuffle-exchange Networks using HOL Theorem Proving

Dynamic dependability models, such as dynamic fault trees (DFTs) and dynamic reliability block diagrams (DRBDs), are introduced to overcome the modeling limitations of traditional models. Recently, higher-order logic (HOL) formalizations of both models have been conducted, which allow the analysis of these models formally, within a theorem prover. In this report, we provide the formal dynamic dependability analysis of shuffle-exchange networks, which are multistage interconnection networks that are commonly used in multiprocessor systems. We use DFTs and DRBDs to model the terminal, broadcast and network reliability with dynamic spare gates and constructs in several generic versions. We verify generic expressions of probability of failure and reliability of these systems, which can be instantiated with any number of system components and failure rates to reason about the failure behavior of these networks.

cs.LO↗

arXiv2019

Integrating DFT and DRBD Formalizations in HOL4

Dynamic Fault Trees (DFT) and Dynamic Reliability Block Diagrams (DRBD) are two modeling approaches that capture the dynamic failure behavior of engineering systems for their reliability analysis. Recently, two independent higher-order logic (HOL) formalizations of DFT and DRBD algebras have been developed in the HOL4 theorem prover. In this work, we propose to integrate these two modeling approaches for the efficient formal reliability analysis of complex systems by leveraging upon the advantages of each method. The soundness of this integration is provided through a formal proof of equivalence between the DFT and DRBD algebras. We show the efficiency of the proposed integrated formal reliability analysis on a drive-by-wire system as a case study.

cs.LO↗

arXiv2019

A Formally Verified HOL Algebra for Dynamic Reliability Block Diagrams

Dynamic reliability block diagrams (DRBDs) are introduced to overcome the modeling limitations of traditional reliability block diagrams, such as the inability to capture redundant components. However, so far there is no algebraic framework that allows conducting the analysis of a given DRBD based on its structure function and enables verifying its soundness using higher-order logic (HOL) theorem proving. In this work, we propose a new algebra to formally express the structure function and the reliability of a DRBD with spare constructs based on basic system blocks and newly introduced DRBD operators. We present several simplification properties that allow reducing the structure of a given DRBD. We provide the HOL formalization of the proposed algebra, and formally verify its corresponding properties using the HOL4 theorem prover. This includes formally verifying generic reliability expressions of the spare construct, series, parallel and deeper structures in an extensible manner that allows verifying the reliability of complex systems. Finally, we demonstrate the applicability of this algebra by formally analyzing the terminal reliability analysis of a shuffle-exchange network in HOL4.

cs.LO↗

arXiv2019

Error Analysis of Approximate Array Multipliers

Approximate computing is a nascent energy-efficient computing paradigm suitable for error-tolerant applications. However, the value of approximation error depends on the applied inputs where individual output error may reach intolerable level while the average output error is acceptable. Thus, it is critical to show the response of approximate design for various applied inputs where understanding the interdependence between the inputs and the approximation error could be utilized to control the output quality. In this report, we exhaustively analyze the accuracy of 20 different designs of 8-bit approximate array multipliers. We designed these multipliers based on various configurations including the type of approximable component and how much of the result to approximate, i.e., approximation degree. Accuracy analysis shows a strong correlation between the applied inputs and the magnitude of the observed error, i.e., error distance, normalized error distance and peak-to-signal-noise ratio. We may utilize this input-dependency of approximation error, in controlling the quality of approximate computing by eliminating large magnitude errors and improving the quality of the final results.

cs.ET↗

arXiv2019

On the Formalization of Importance Measures using HOL Theorem Proving

Importance measures provide a systematic approach to scrutinize critical system components, which are extremely beneficial in making important decisions, such as prioritizing reliability improvement activities, identifying weak-links and effective usage of given resources. The importance measures are then in turn used to obtain a criticality value for each system component and to rank the components in descending manner. Simulations tools are generally used to perform importance measure based analysis, but they require expensive computations and thus they are not suitable for large systems. A more scalable approach is to utilize the importance measures to obtain all the necessary conditions by proving a generic relationship describing the relative importance between any pair of components in a system. In this paper, we propose to use higher-order-logic (HOL) theorem proving to verify such relationships and thus making sure that all the essential conditions are accompanied by the proven property. In particular, we formalize the commonly used importance measures, such as Birnbaum and Fussell-Vesely, and conduct a formal importance measure analysis of a railway signaling system at a Moroccan level crossing as an application for illustration purpose.

cs.FL↗

arXiv2018

ApproxCS: Near-Sensor Approximate Compressed Sensing for IoT-Healthcare Systems

Internet of Things (IoTs) is an emerging trend that has enabled an upgrade in the design of wearable healthcare monitoring systems through the (integrated) edge, fog, and cloud computing paradigm. Energy efficiency is one of the most important design metrics in such IoT-healthcare systems especially, for the edge and fog nodes. Due to the sensing noise and inherent redundancy in the input data, even the most safety-critical biomedical applications can sometimes afford a slight degradation in the output quality. Hence, such inherent error tolerance in the bio-signals can be exploited to achieve high energy savings through the emerging trends like, the Approximate Computing which is applicable at both software and hardware levels. In this paper, we propose to leverage the approximate computing in digital Compressed Sensing (CS), through low-power approximate adders (LPAA) in an accurate Bernoulli sensing-based CS acquisition (BCS). We demonstrate that approximations can indeed be safely employed in IoT healthcare without affecting the detection of critical events in the biomedical signals. Towards this, we explored the trade-of between energy efficiency and output quality using the state-of-the-art lp2d RLS reconstruction algorithm. The proposed framework is validated with the MIT-BIH Arrhythmia database. Our results demonstrated approximately 59% energy savings as compared to the accurate design.

eess.SP↗

arXiv2018

Formal Probabilistic Analysis of Dynamic Fault Trees in HOL4

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<Y), using the Lebesgue integral as this relationship allows us to reason about the probabilistic properties of Priority-AND gate and the Before operator. We also formalize the notion of conditional densities in order to formally verify the probabilistic expressions of the Cold SPare and the Warm SPare gates. For illustrating the usefulness of our formalization, we use it to formally analyze the DFT of a Cardiac Assist System.

cs.LO↗

arXiv2018

Formal Modeling of Robotic Cell Injection Systems in Higher-order Logic

Robotic cell injection is used for automatically delivering substances into a cell and is an integral component of drug development, genetic engineering and many other areas of cell biology. Traditionally, the correctness of functionality of these systems is ascertained using paper-and-pencil proof and computer simulation methods. However, the paper based proofs can be human-error prone and the simulation provides an incomplete analysis due to its sampling based nature and the inability to capture continuous behaviors in computer based models. Model checking has been recently advocated for the analysis of cell injection systems as well. However, it involves the discretization of the differential equations that are used for modeling the dynamics of the system and thus compromises on the completeness of the analysis as well. In this paper, we propose to use higher-order-logic theorem proving for the modeling and analysis of the dynamical behaviour of the robotic cell injection systems. The high expressiveness of the underlying logic allows us to capture the continuous details of the model in their true form. Then, the model can be analyzed using deductive reasoning within the sound core of a proof assistant.

cs.LO↗

arXiv2018

Formalization of Lerch's Theorem using HOL Light

The Laplace transform is an algebraic method that is widely used for analyzing physical systems by either solving the differential equations modeling their dynamics or by evaluating their transfer function. The dynamics of the given system are firstly modeled using differential equations and then Laplace transform is applied to convert these differential equations to their equivalent algebraic equations. These equations can further be simplified to either obtain the transfer function of the system or to find out the solution of the differential equations in frequency domain. Next, the uniqueness of the Laplace transform provides the solution of these differential equations in the time domain. The traditional Laplace transform based analysis techniques, i.e., paper-and-pencil proofs and computer simulation methods are error-prone due to their inherent limitations and thus are not suitable for the analysis of the systems. Higher-order-logic theorem proving can overcome these limitations of these techniques and can ascertain accurate analysis of the systems. In this paper, we extend our higher-order logic formalization of the Laplace transform, which includes the formal definition of the Laplace transform and verification of its various classical properties. One of the main contributions of the paper is the formalization of Lerch's theorem, which describes the uniqueness of the Laplace transform and thus plays a vital role in solving linear differential equations in the frequency domain. For illustration, we present the formal analysis of a $4$-$π$ soft error crosstalk model, which is widely used in nanometer technologies, such as, Integrated Circuits (ICs).

cs.LO↗

arXiv2018

Formal Analysis of Robotic Cell Injection Systems using Theorem Proving

Cell injection is an approach used for the delivery of small sample substances into a biological cell and is widely used in drug development, gene injection, intracytoplasmic sperm injection (ICSI) and in-virto fertilization (IVF). Robotic cell injection systems provide the automation of the process as opposed to the manual and semi-automated cell injection systems, which require expert operators and involve time consuming processes and also have lower success rates. The automation of the cell injection process is achieved by controlling the injection force and planning the motion of the injection pipette. Traditionally, these systems are analyzed using paper-and-pencil proof and computer simulation methods. However, the former is human-error prone and the later is based on the numerical algorithms, where the approximation of the mathematical expressions introduces inaccuracies in the analysis. Formal methods can overcome these limitations and thus provide an accurate analysis of the cell injection systems. Model checking, i.e., a state-based formal method, has been recently proposed for the analysis of these systems. However, it involves the discretization of the differential equations that are used for modeling the dynamics of the system and thus compromises on the completeness of the analysis of these safety-critical systems. In this paper, we propose to use higher-order-logic theorem proving, a deductive-reasoning based formal method, for the modeling and analysis of the dynamical behaviour of the robotic cell injection systems. The proposed analysis, based on the HOL Light theorem prover, enabled us to identify some discrepancies in the simulation and model checking based analysis of the same robotic cell injection system.

cs.LO↗

arXiv2018

Formal Verification of Platoon Control Strategies

Recent developments in autonomous driving, vehicle-to-vehicle communication and smart traffic controllers have provided a hope to realize platoon formation of vehicles. The main benefits of vehicle platooning include improved safety, enhanced highway utility, efficient fuel consumption and reduced highway accidents. One of the central components of reliable and efficient platoon formation is the underlying control strategies, e.g., constant spacing, variable spacing and dynamic headway. In this paper, we provide a generic formalization of platoon control strategies in higher-order logic. In particular, we formally verify the stability constraints of various strategies using the libraries of multivariate calculus and Laplace transform within the sound core of HOL Light proof assistant. We also illustrate the use of verified stability theorems to develop runtime monitors for each controller, which can be used to automatically detect the violation of stability constraints in a runtime execution or a logged trace of the platoon controller. Our proposed formalization has two main advantages: 1) it provides a framework to combine both static (theorem proving) and dynamic (runtime) verification approaches for platoon controllers, and 2) it is inline with the industrial standards, which explicitly recommend the use of formal methods for functional safety, e.g., automotive ISO 26262.

cs.LO↗

arXiv2018

Comparative Study of Approximate Multipliers

Approximate multipliers are widely being advocated for energy-efficient computing in applications that exhibit an inherent tolerance to inaccuracy. However, the inclusion of accuracy as a key design parameter, besides the performance, area and power, makes the identification of the most suitable approximate multiplier quite challenging. In this paper, we identify three major decision making factors for the selection of an approximate multipliers circuit: (1) the type of approximate full adder (FA) used to construct the multiplier, (2) the architecture, i.e., array or tree, of the multiplier and (3) the placement of sub-modules of approximate and exact multipliers in the main multiplier module. Based on these factors, we explored the design space for circuit level implementations of approximate multipliers. We used circuit level implementations of some of the most widely used approximate full adders, i.e., approximate mirror adders, XOR/XNOR based approximate full adders and Inexact adder cell. These FA cells are then used to develop circuits for the approximate high order compressors as building blocks for 8x8 array and tree multipliers. We then develop various implementations of higher bit multipliers by using a combination of exact and inaccurate 8x8 multiplier cells. All these implementations have been done using the Cadence's Spectre tool with the TSMC65nm technology. The design space of these multipliers is explored based on their power, area, delay and error and the best approximate multiplier designs are identified. The report also presents the validation of our results using an image blending application. An open source library of implemented cells and multiplier circuits are available online.

cs.ET↗

arXiv2017

Dynamic Fault Trees Analysis using an Integration of Theorem Proving and Model Checking

Dynamic fault trees (DFTs) have emerged as an important tool for capturing the dynamic behavior of system failure. These DFTs are then analyzed qualitatively and quantitatively using stochastic or algebraic methods to judge the failure characteristics of the given system in terms of the failures of its sub-components. Model checking has been recently proposed to conduct the failure analysis of systems using DFTs with the motivation to provide a rigorous failure analysis of safety-critical systems. However, model checking has not been used for the DFT qualitative analysis and the reduction algorithms used in model checking are usually not formally verified. Moreover, the analysis time grows exponentially with the increase of the number of states. These issues limit the usefulness of model checking for analyzing complex systems used in safety-critical domains, where the accuracy and completeness of analysis matters the most. To overcome these limitations, we propose a comprehensive methodology to perform the qualitative and quantitative analysis of DFTs using an integration of theorem proving and model checking based approaches. For this purpose, we formalized all the basic dynamic fault tree gates using higher-order logic based on the algebraic approach and formally verified some of the simplification properties. This formalization allows us to formally verify the equivalence between the original and reduced DFTs using a theorem prover, and conduct the qualitative analysis. We then use model checking to perform the quantitative analysis of the formally verified reduced DFT. We applied our methodology to five benchmarks and the results show that the formally verified reduced DFT was analyzed using model checking with up to six times less states and up to 133000 times faster.

cs.LO↗

arXiv2017

Formal Analysis of Continuous-time Systems using Fourier Transform

To study the dynamical behaviour of the engineering and physical systems, we often need to capture their continuous behaviour, which is modeled using differential equations, and perform the frequency-domain analysis of these systems. Traditionally, Fourier transform methods are used to perform this frequency domain analysis using paper-and-pencil based analytical techniques or computer simulations. However, both of these methods are error prone and thus are not suitable for analyzing systems used in safety-critical domains, like medicine and transportation. In order to provide an accurate alternative, we propose to use higher-order-logic theorem proving to conduct the frequency domain analysis of these systems. For this purpose, the paper presents a higher-order-logic formalization of Fourier transform using the HOL-Light theorem prover. In particular, we use the higher-order-logic based formalizations of differential, integral, transcendental and topological theories of multivariable calculus to formally define Fourier transform and reason about the correctness of its classical properties, such as existence, linearity, time shifting, frequency shifting, modulation, time scaling, time reversal and differentiation in time domain, and its relationships with Fourier Cosine, Fourier Sine and Laplace transforms. We use our proposed formalization for the formal verification of the frequency response of a generic n-order linear system, an audio equalizer and a MEMs accelerometer, using the HOL-Light theorem prover.

cs.LO↗

arXiv2017

Formal Analysis of Linear Control Systems using Theorem Proving

Control systems are an integral part of almost every engineering and physical system and thus their accurate analysis is of utmost importance. Traditionally, control systems are analyzed using paper-and-pencil proof and computer simulation methods, however, both of these methods cannot provide accurate analysis due to their inherent limitations. Model checking has been widely used to analyze control systems but the continuous nature of their environment and physical components cannot be truly captured by a state-transition system in this technique. To overcome these limitations, we propose to use higher-order-logic theorem proving for analyzing linear control systems based on a formalized theory of the Laplace transform method. For this purpose, we have formalized the foundations of linear control system analysis in higher-order logic so that a linear control system can be readily modeled and analyzed. The paper presents a new formalization of the Laplace transform and the formal verification of its properties that are frequently used in the transfer function based analysis to judge the frequency response, gain margin and phase margin, and stability of a linear control system. We also formalize the active realizations of various controllers, like Proportional-Integral-Derivative (PID), Proportional-Integral (PI), Proportional-Derivative (PD), and various active and passive compensators, like lead, lag and lag-lead. For illustration, we present a formal analysis of an unmanned free-swimming submersible vehicle using the HOL Light theorem prover.

cs.LO↗

arXiv2017

Formalization of Transform Methods using HOL Light

Transform methods, like Laplace and Fourier, are frequently used for analyzing the dynamical behaviour of engineering and physical systems, based on their transfer function, and frequency response or the solutions of their corresponding differential equations. In this paper, we present an ongoing project, which focuses on the higher-order logic formalization of transform methods using HOL Light theorem prover. In particular, we present the motivation of the formalization, which is followed by the related work. Next, we present the task completed so far while highlighting some of the challenges faced during the formalization. Finally, we present a roadmap to achieve our objectives, the current status and the future goals for this project.

cs.LO↗

arXiv2017

Towards Probabilistic Formal Modeling of Robotic Cell Injection Systems

Cell injection is a technique in the domain of biological cell micro-manipulation for the delivery of small volumes of samples into the suspended or adherent cells. It has been widely applied in various areas, such as gene injection, in-vitro fertilization (IVF), intracytoplasmic sperm injection (ISCI) and drug development. However, the existing manual and semi-automated cell injection systems require lengthy training and suffer from high probability of contamination and low success rate. In the recently introduced fully automated cell injection systems, the injection force plays a vital role in the success of the process since even a tiny excessive force can destroy the membrane or tissue of the biological cell. Traditionally, the force control algorithms are analyzed using simulation, which is inherently non-exhaustive and incomplete in terms of detecting system failures. Moreover, the uncertainties in the system are generally ignored in the analysis. To overcome these limitations, we present a formal analysis methodology based on probabilistic model checking to analyze a robotic cell injection system utilizing the impedance force control algorithm. The proposed methodology, developed using the PRISM model checker, allowed to find a discrepancy in the algorithm, which was not found by any of the previous analysis using the traditional methods.

cs.LO↗