Source author record

Osman Hasan

Osman Hasan appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Catalog footprint

What is connected

18works
9topics
4close collaborators

Actions

Connect this record

Log in to claim

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

18 published item(s)

preprint2022arXiv

Continual Learning for Real-World Autonomous Systems: Algorithms, Challenges and Frameworks

Continual learning is essential for all real-world applications, as frozen pre-trained models cannot effectively deal with non-stationary data distributions. The purpose of this study is to review the state-of-the-art methods that allow continuous learning of computational models over time. We primarily focus on the learning algorithms that perform continuous learning in an online fashion from considerably large (or infinite) sequential data and require substantially low computational and memory resources. We critically analyze the key challenges associated with continual learning for autonomous real-world systems and compare current methods in terms of computations, memory, and network/model complexity. We also briefly describe the implementations of continuous learning algorithms under three main autonomous systems, i.e., self-driving vehicles, unmanned aerial vehicles, and urban robots. The learning methods of these autonomous systems and their strengths and limitations are extensively explored in this article.

preprint2022arXiv

On the Formalization of the Heat Conduction Problem in HOL

Partial Differential Equations (PDEs) are widely used for modeling the physical phenomena and analyzing the dynamical behavior of many engineering and physical systems. The heat equation is one of the most well-known PDEs that captures the temperature distribution and diffusion of heat within a body. Due to the wider utility of these equations in various safety-critical applications, such as thermal protection systems, a formal analysis of the heat transfer is of utmost importance. In this paper, we propose to use higher-order-logic (HOL) theorem proving for formally analyzing the heat conduction problem in rectangular coordinates. In particular, we formally model the heat transfer as a one-dimensional heat equation for a rectangular slab using the multivariable calculus theories of the HOL Light theorem prover. This requires the formalization of the heat operator and formal verification of its various properties, such as linearity and scaling. Moreover, we use the separation of variables method for formally verifying the solution of the PDEs, which allows modeling the heat transfer in the slab under various initial and boundary conditions using HOL Light.

preprint2020arXiv

FANNet: Formal Analysis of Noise Tolerance, Training Bias and Input Sensitivity in Neural Networks

With a constant improvement in the network architectures and training methodologies, Neural Networks (NNs) are increasingly being deployed in real-world Machine Learning systems. However, despite their impressive performance on "known inputs", these NNs can fail absurdly on the "unseen inputs", especially if these real-time inputs deviate from the training dataset distributions, or contain certain types of input noise. This indicates the low noise tolerance of NNs, which is a major reason for the recent increase of adversarial attacks. This is a serious concern, particularly for safety-critical applications, where inaccurate results lead to dire consequences. We propose a novel methodology that leverages model checking for the Formal Analysis of Neural Network (FANNet) under different input noise ranges. Our methodology allows us to rigorously analyze the noise tolerance of NNs, their input node sensitivity, and the effects of training bias on their performance, e.g., in terms of classification accuracy. For evaluation, we use a feed-forward fully-connected NN architecture trained for the Leukemia classification. Our experimental results show $\pm 11\%$ noise tolerance for the given trained network, identify the most sensitive input nodes, and confirm the biasness of the available training dataset.

preprint2020arXiv

FASiM: A Framework for Automatic Formal Analysis of Simulink Models of Linear Analog Circuits

Simulink is a graphical environment that is widely adapted for the modeling and the Laplace transform based analysis of linear analog circuits used in signal processing architectures. However, due to the involvement of the numerical algorithms of MATLAB in the analysis process, the analysis results cannot be termed as complete and accurate. Higher-order-logic theorem proving is a formal verification method that has been recently proposed to overcome these limitations for the modeling and the Laplace transform based analysis of linear analog circuits. However, the formal modeling of a system is not a straightforward task due to the lack of formal methods background for engineers working in the industry. Moreover, due to the undecidable nature of higher-order logic, the analysis generally requires a significant amount of user guidance in the manual proof process. In order to facilitate industrial engineers to formally analyze the linear analog circuits based on the Laplace transform, we propose a framework, FASiM, which allows automatically conducting the formal analysis of the Simulink models of linear analog circuits using the HOL Light theorem prover. For illustration, we use FASiM to formally analyze Simulink models of some commonly used linear analog filters, such as Sallen-key filters.

preprint2020arXiv

Machine Learning-Based Self-Compensating Approximate Computing

Dedicated hardware accelerators are suitable for parallel computational tasks. Moreover, they have the tendency to accept inexact results. These hardware accelerators are extensively used in image processing and computer vision applications, e.g., to process the dense 3-D maps required for self-driving cars. Such error-tolerant hardware accelerators can be designed approximately for reduced power consumption and/or processing time. However, since for some inputs the output errors may reach unacceptable levels, the main challenge is to \textit{enhance the accuracy} of the results of approximate accelerators and keep the error magnitude within an allowed range. Towards this goal, in this paper, we propose a novel machine learning-based self-compensating approximate accelerators for energy efficient systems. The proposed error \textit{compensation module}, which is integrated within the architecture of approximate hardware accelerators, efficiently reduces the accumulated error at its output. It utilizes \textit{lightweight supervised machine learning techniques, i.e., decision tree}, to capture input dependency of the error. We consider image blending application in multiplication mode to demonstrate a practical application of self-compensating approximate computing. Simulation results show that the proposed design of self-compensating approximate accelerator can achieve about 9\% accuracy enhancement, with negligible overhead in other performance measures, i.e., power, area, delay and energy.

preprint2020arXiv

SIMCom: Statistical Sniffing of Inter-Module Communications for Run-time Hardware Trojan Detection

Timely detection of Hardware Trojans (HTs) has become a major challenge for secure integrated circuits. We present a run-time methodology for HT detection that employs a multi-parameter statistical traffic modeling of the communication channel in a given System-on-Chip (SoC), named as SIMCom. The main idea is to model the communication using multiple side-channel information like the Hurst exponent, the standard deviation of the injection distribution, and the hop distribution jointly to accurately identify HT-based online anomalies (that affects the communication without affecting the protocols or control signals). At design time, our methodology employs a "property specification language" to define and embed assertions in the RTL, specifying the correct communication behavior of a given SoC. At run-time, it monitors the anomalies in the communication behavior by checking the execution patterns against these assertions. For illustration, we evaluate SIMCom for three SoCs, i.e., SoC1 ( four single-core MC8051 and UART modules), SoC2 (four single-core MC8051, AES, ethernet, memctrl, BasicRSA, RS232 modules), and SoC3 (four single-core LEON3 connected with each other and AES, ethernet, memctrl, BasicRSA, RS23s modules microcontrollers). The experimental results show that with the combined analysis of multiple statistical parameters, SIMCom is able to detect all the benchmark Trojans (available on trust-hub) with less than 1% area and power overhead.

preprint2016arXiv

Formal Availability Analysis using Theorem Proving

Availability analysis is used to assess the possible failures and their restoration process for a given system. This analysis involves the calculation of instantaneous and steady-state availabilities of the individual system components and the usage of this information along with the commonly used availability modeling techniques, such as Availability Block Diagrams (ABD) and Fault Trees (FTs) to determine the system-level availability. Traditionally, availability analyses are conducted using paper-and-pencil methods and simulation tools but they cannot ascertain absolute correctness due to their inaccuracy limitations. As a complementary approach, we propose to use the higher-order-logic theorem prover HOL4 to conduct the availability analysis of safety-critical systems. For this purpose, we present a higher-order-logic formalization of instantaneous and steady-state availability, ABD configurations and generic unavailability FT gates. For illustration purposes, these formalizations are utilized to conduct formal availability analysis of a satellite solar array, which is used as the main source of power for the Dong Fang Hong-3 (DFH-3) satellite.

preprint2016arXiv

Formal Dependability Modeling and Analysis: A Survey

Dependability is an umbrella concept that subsumes many key properties about a system, including reliability, maintainability, safety, availability, confidentiality, and integrity. Various dependability modeling techniques have been developed to effectively capture the failure characteristics of systems over time. Traditionally, dependability models are analyzed using paper-and-pencil proof methods and computer based simulation tools but their results cannot be trusted due to their inherent inaccuracy limitations. The recent developments in probabilistic analysis support using formal methods have enabled the possibility of accurate and rigorous dependability analysis. Thus, the usage of formal methods for dependability analysis is widely advocated for safety-critical domains, such as transportation, aerospace and health. Given the complementary strengths of mainstream formal methods, like theorem proving and model checking, and the variety of dependability models judging the most suitable formal technique for a given dependability model is not a straightforward task. In this paper, we present a comprehensive review of existing formal dependability analysis techniques along with their pros and cons for handling a particular dependability model.

preprint2016arXiv

Formalization of Fault Trees in Higher-order Logic: A Deep Embedding Approach

Fault Tree (FT) is a standard failure modeling technique that has been extensively used to predict reliability, availability and safety of many complex engineering systems. In order to facilitate the formal analysis of FT based analyses, a higher-order-logic formalization of FTs has been recently proposed. However, this formalization is quite limited in terms of handling large systems and transformation of FT models into their corresponding Reliability Block Diagram (RBD) structures, i.e., a frequently used transformation in reliability and availability analyses. In order to overcome these limitations, we present a deep embedding based formalization of FTs. In particular, the paper presents a formalization of AND, OR and NOT FT gates, which are in turn used to formalize other commonly used FT gates, i.e., NAND, NOR, XOR, Inhibit, Comparator and majority Voting, and the formal verification of their failure probability expressions. For illustration purposes, we present a formal failure analysis of a communication gateway software for the next generation air traffic management system.

preprint2016arXiv

Reliability Modeling and Analysis of Communication Networks

In recent times, the functioning of various aspects of modern society---ranging from the various infrastructural utilities such as electrical power, water to socio-economical aspects such as telecommunications, business, commerce, education---has become critically reliant on communication networks, and particularly on the Internet. With the migration of critical facilities to the Internet, it has become vitally important to ensure the reliability and availability of networks. In this paper, we study various modeling and analysis techniques that can aid in the study of reliability of communication networks. In this regard, we provide background on the modeling techniques (such as reliability block diagrams, fault trees, Markov chains, etc.) and analysis techniques (such as mathematical analytical methods, simulation methods, and formal methods). Apart from providing the necessary background, we also critically evaluate the pros and cons of different approaches, and provide a detailed survey of their applications in communication networks. To the best of our knowledge, this is the first in-depth review of the application of reliability modeling and analysis techniques in communication networks.

preprint2015arXiv

Towards Formal Fault Tree Analysis using Theorem Proving

Fault Tree Analysis (FTA) is a dependability analysis technique that has been widely used to predict reliability, availability and safety of many complex engineering systems. Traditionally, these FTA-based analyses are done using paper-and-pencil proof methods or computer simulations, which cannot ascertain absolute correctness due to their inherent limitations. As a complementary approach, we propose to use the higher-order-logic theorem prover HOL4 to conduct the FTA-based analysis of safety-critical systems where accuracy of failure analysis is a dire need. In particular, the paper presents a higher-order-logic formalization of generic Fault Tree gates, i.e., AND, OR, NAND, NOR, XOR and NOT and the formal verification of their failure probability expressions. Moreover, we have formally verified the generic probabilistic inclusion-exclusion principle, which is one of the foremost requirements for conducting the FTA-based failure analysis of any given system. For illustration purposes, we conduct the FTA-based failure analysis of a solar array that is used as the main source of power for the Dong Fang Hong-3 (DFH-3) satellite.

preprint2015arXiv

Towards the Formalization of Fractional Calculus in Higher-Order Logic

Fractional calculus is a generalization of classical theories of integration and differentiation to arbitrary order (i.e., real or complex numbers). In the last two decades, this new mathematical modeling approach has been widely used to analyze a wide class of physical systems in various fields of science and engineering. In this paper, we describe an ongoing project which aims at formalizing the basic theories of fractional calculus in the HOL Light theorem prover. Mainly, we present the motivation and application of such formalization efforts, a roadmap to achieve our goals, current status of the project and future milestones.

preprint2014arXiv

Formal Analysis of Optical Systems

Optical systems are becoming increasingly important by resolving many bottlenecks in today's communication, electronics, and biomedical systems. However, given the continuous nature of optics, the inability to efficiently analyze optical system models using traditional paper-and-pencil and computer simulation approaches sets limits especially in safety-critical applications. In order to overcome these limitations, we propose to employ higher-order-logic theorem proving as a complement to computational and numerical approaches to improve optical model analysis in a comprehensive framework. The proposed framework allows formal analysis of optical systems at four abstraction levels, i.e., ray, wave, electromagnetic, and quantum.

preprint2014arXiv

Formalization of Complex Vectors in Higher-Order Logic

Complex vector analysis is widely used to analyze continuous systems in many disciplines, including physics and engineering. In this paper, we present a higher-order-logic formalization of the complex vector space to facilitate conducting this analysis within the sound core of a theorem prover: HOL Light. Our definition of complex vector builds upon the definitions of complex numbers and real vectors. This extension allows us to extensively benefit from the already verified theorems based on complex analysis and real vector analysis. To show the practical usefulness of our library we adopt it to formalize electromagnetic fields and to prove the law of reflection for the planar waves.

preprint2014arXiv

Towards the Formal Reliability Analysis of Oil and Gas Pipelines

It is customary to assess the reliability of underground oil and gas pipelines in the presence of excessive loading and corrosion effects to ensure a leak-free transport of hazardous materials. The main idea behind this reliability analysis is to model the given pipeline system as a Reliability Block Diagram (RBD) of segments such that the reliability of an individual pipeline segment can be represented by a random variable. Traditionally, computer simulation is used to perform this reliability analysis but it provides approximate results and requires an enormous amount of CPU time for attaining reasonable estimates. Due to its approximate nature, simulation is not very suitable for analyzing safety-critical systems like oil and gas pipelines, where even minor analysis flaws may result in catastrophic consequences. As an accurate alternative, we propose to use a higher-order-logic theorem prover (HOL) for the reliability analysis of pipelines. As a first step towards this idea, this paper provides a higher-order-logic formalization of reliability and the series RBD using the HOL theorem prover. For illustration, we present the formal analysis of a simple pipeline that can be modeled as a series RBD of segments with exponentially distributed failure times.

preprint2013arXiv

Applying Formal Methods to Networking: Theory, Techniques and Applications

Despite its great importance, modern network infrastructure is remarkable for the lack of rigor in its engineering. The Internet which began as a research experiment was never designed to handle the users and applications it hosts today. The lack of formalization of the Internet architecture meant limited abstractions and modularity, especially for the control and management planes, thus requiring for every new need a new protocol built from scratch. This led to an unwieldy ossified Internet architecture resistant to any attempts at formal verification, and an Internet culture where expediency and pragmatism are favored over formal correctness. Fortunately, recent work in the space of clean slate Internet design---especially, the software defined networking (SDN) paradigm---offers the Internet community another chance to develop the right kind of architecture and abstractions. This has also led to a great resurgence in interest of applying formal methods to specification, verification, and synthesis of networking protocols and applications. In this paper, we present a self-contained tutorial of the formidable amount of work that has been done in formal methods, and present a survey of its applications to networking.

preprint2013arXiv

Formal Analysis of Soft Errors using Theorem Proving

Modeling and analysis of soft errors in electronic circuits has traditionally been done using computer simulations. Computer simulations cannot guarantee correctness of analysis because they utilize approximate real number representations and pseudo random numbers in the analysis and thus are not well suited for analyzing safety-critical applications. In this paper, we present a higher-order logic theorem proving based method for modeling and analysis of soft errors in electronic circuits. Our developed infrastructure includes formalized continuous random variable pairs, their Cumulative Distribution Function (CDF) properties and independent standard uniform and Gaussian random variables. We illustrate the usefulness of our approach by modeling and analyzing soft errors in commonly used dynamic random access memory sense amplifier circuits.

preprint2013arXiv

Formal Probabilistic Analysis of a Wireless Sensor Network for Forest Fire Detection

Wireless Sensor Networks (WSNs) have been widely explored for forest fire detection, which is considered a fatal threat throughout the world. Energy conservation of sensor nodes is one of the biggest challenges in this context and random scheduling is frequently applied to overcome that. The performance analysis of these random scheduling approaches is traditionally done by paper-and-pencil proof methods or simulation. These traditional techniques cannot ascertain 100% accuracy, and thus are not suitable for analyzing a safety-critical application like forest fire detection using WSNs. In this paper, we propose to overcome this limitation by applying formal probabilistic analysis using theorem proving to verify scheduling performance of a real-world WSN for forest fire detection using a k-set randomized algorithm as an energy saving mechanism. In particular, we formally verify the expected values of coverage intensity, the upper bound on the total number of disjoint subsets, for a given coverage intensity, and the lower bound on the total number of nodes.