arXiv subjects

Osman Hasan

Publications and source records attributed to Osman Hasan.

At least 19 recordsLinked to original sources

arXiv2026

On the Formalization of Network Topology Matrices in HOL

Network topology matrices are algebraic representations of graphs that are widely used in modeling and analysis of various applications including electrical circuits, communication networks and transportation systems. In this paper, we propose to use Higher-Order-Logic (HOL) based interactive theorem proving to formalize network topology matrices. In particular, we formalize adjacency, degree, Laplacian and incidence matrices in the Isabelle/HOL proof assistant. Our formalization is based on modelling systems as networks using the notion of directed graphs (unweighted and weighted), where nodes act as components of the system and weighted edges capture the interconnection between them. Then, we formally verify various classical properties of these matrices, such as indexing and degree. We also prove the relationships between these matrices in order to provide a comprehensive formal reasoning support for analyzing systems modeled using network topology matrices. To illustrate the effectiveness of the proposed approach, we formally analyze the Kron reduction of the Laplacian matrix and verify the total power dissipation in a generic resistive electrical network, both commonly used in power flow analysis.

cs.LO↗

arXiv2025

Replay4NCL: An Efficient Memory Replay-based Methodology for Neuromorphic Continual Learning in Embedded AI Systems

Neuromorphic Continual Learning (NCL) paradigm leverages Spiking Neural Networks (SNNs) to enable continual learning (CL) capabilities for AI systems to adapt to dynamically changing environments. Currently, the state-of-the-art employ a memory replay-based method to maintain the old knowledge. However, this technique relies on long timesteps and compression-decompression steps, thereby incurring significant latency and energy overheads, which are not suitable for tightly-constrained embedded AI systems (e.g., mobile agents/robotics). To address this, we propose Replay4NCL, a novel efficient memory replay-based methodology for enabling NCL in embedded AI systems. Specifically, Replay4NCL compresses the latent data (old knowledge), then replays them during the NCL training phase with small timesteps, to minimize the processing latency and energy consumption. To compensate the information loss from reduced spikes, we adjust the neuron threshold potential and learning rate settings. Experimental results on the class-incremental scenario with the Spiking Heidelberg Digits (SHD) dataset show that Replay4NCL can preserve old knowledge with Top-1 accuracy of 90.43% compared to 86.22% from the state-of-the-art, while effectively learning new tasks, achieving 4.88x latency speed-up, 20% latent memory saving, and 36.43% energy saving. These results highlight the potential of our Replay4NCL methodology to further advances NCL capabilities for embedded AI systems.

cs.NE↗

arXiv2024

Formalization of Biological Circuit Block Diagrams for formally analyzing Biomedical Control Systems in pHRI Applications

The control of Biomedical Systems in Physical Human-Robot Interaction (pHRI) plays a pivotal role in achieving the desired behavior by ensuring the intended transfer function and stability of subsystems within the overall system. Traditionally, the control aspects of biomedical systems have been analyzed using manual proofs and computer based analysis tools. However, these approaches provide inaccurate results due to human error in manual proofs and unverified algorithms and round-off errors in computer-based tools. We argue using Interactive reasoning, or frequently called theorem proving, to analyze control systems of biomedical engineering applications, specifically in the context of Physical Human-Robot Interaction (pHRI). Our methodology involves constructing mathematical models of the control components using Higher-order Logic (HOL) and analyzing them through deductive reasoning in the HOL Light theorem prover. We propose to model these control systems in terms of their block diagram representations, which in turn utilize the corresponding differential equations and their transfer function-based representation using the Laplace Transform (LT). These formally represented block diagrams are then analyzed through logical reasoning in the trusted environment of a theorem prover to ensure the correctness of the results. For illustration, we present a real-world case study by analyzing the control system of the ultrafilteration dialysis process.

cs.LO↗

arXiv2024

Continual Learning with Neuromorphic Computing: Foundations, Methods, and Emerging Applications

The challenging deployment of compute- and memory-intensive methods from Deep Neural Network (DNN)-based Continual Learning (CL) underscores the critical need for a paradigm shift towards more efficient approaches. Neuromorphic Continual Learning (NCL) appears as an emerging solution, by leveraging the principles of Spiking Neural Networks (SNNs) which enable efficient CL algorithms executed in dynamically-changed environments with resource-constrained computing systems. Motivated by the need for a holistic study of NCL, in this survey, we first provide a detailed background on CL, encompassing the desiderata, settings, metrics, scenario taxonomy, Online Continual Learning (OCL) paradigm, recent DNN-based methods to address catastrophic forgetting (CF). Then, we analyze these methods considering CL desiderata, computational and memory costs, as well as network complexity, hence emphasizing the need for energy-efficient CL. Afterward, we provide background of low-power neuromorphic systems including encoding techniques, neuronal dynamics, network architectures, learning rules, hardware processors, software and hardware frameworks, datasets, benchmarks, and evaluation metrics. Then, this survey comprehensively reviews and analyzes state-of-the-art in NCL. The key ideas, implementation frameworks, and performance assessments are also provided. This survey covers several hybrid approaches that combine supervised and unsupervised learning paradigms. It also covers optimization techniques including SNN operations reduction, weight quantization, and knowledge distillation. Then, this survey discusses the progress of real-world NCL applications. Finally, this paper provides a future perspective on the open research challenges for NCL, since the purpose of this study is to be useful for the wider neuromorphic AI research community and to inspire future research in bio-plausible OCL.

cs.NE↗

arXiv2023

Scaling Model Checking for DNN Analysis via State-Space Reduction and Input Segmentation (Extended Version)

Owing to their remarkable learning capabilities and performance in real-world applications, the use of machine learning systems based on Neural Networks (NNs) has been continuously increasing. However, various case studies and empirical findings in the literature suggest that slight variations to NN inputs can lead to erroneous and undesirable NN behavior. This has led to considerable interest in their formal analysis, aiming to provide guarantees regarding a given NN's behavior. Existing frameworks provide robustness and/or safety guarantees for the trained NNs, using satisfiability solving and linear programming. We proposed FANNet, the first model checking-based framework for analyzing a broader range of NN properties. However, the state-space explosion associated with model checking entails a scalability problem, making the FANNet applicable only to small NNs. This work develops state-space reduction and input segmentation approaches, to improve the scalability and timing efficiency of formal NN analysis. Compared to the state-of-the-art FANNet, this enables our new model checking-based framework to reduce the verification's timing overhead by a factor of up to 8000, making the framework applicable to NNs even with approximately $80$ times more network parameters. This in turn allows the analysis of NN safety properties using the new framework, in addition to all the NN properties already included with FANNet. The framework is shown to be efficiently able to analyze properties of NNs trained on healthcare datasets as well as the well--acknowledged ACAS Xu NNs.

cs.LG↗

arXiv2023

UnbiasedNets: A Dataset Diversification Framework for Robustness Bias Alleviation in Neural Networks

Performance of trained neural network (NN) models, in terms of testing accuracy, has improved remarkably over the past several years, especially with the advent of deep learning. However, even the most accurate NNs can be biased toward a specific output classification due to the inherent bias in the available training datasets, which may propagate to the real-world implementations. This paper deals with the robustness bias, i.e., the bias exhibited by the trained NN by having a significantly large robustness to noise for a certain output class, as compared to the remaining output classes. The bias is shown to result from imbalanced datasets, i.e., the datasets where all output classes are not equally represented. Towards this, we propose the UnbiasedNets framework, which leverages K-means clustering and the NN's noise tolerance to diversify the given training dataset, even from relatively smaller datasets. This generates balanced datasets and reduces the bias within the datasets themselves. To the best of our knowledge, this is the first framework catering to the robustness bias problem in NNs. We use real-world datasets to demonstrate the efficacy of the UnbiasedNets for data diversification, in case of both binary and multi-label classifiers. The results are compared to well-known tools aimed at generating balanced datasets, and illustrate how existing works have limited success while addressing the robustness bias. In contrast, UnbiasedNets provides a notable improvement over existing works, while even reducing the robustness bias significantly in some cases, as observed by comparing the NNs trained on the diversified and original datasets.

cs.LG↗

arXiv2022

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.

cs.LO↗

arXiv2022

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.

cs.LG↗

arXiv2021

Towards the Formal Performance Analysis of Multistate Coherent Systems using HOL Theorem Proving

Many practical engineering systems and their components have multiple performance levels and failure modes. If these systems form a monotonically increasing structure function (system model) with respect to the performance of their components and also if all of their components affect the overall system performance, then they are said to be multistate coherent systems. Traditionally, the reliability analysis of these multistate coherent systems has been carried out using paper-and-pencil or simulation based methods. The former method is often prone to human errors, while the latter requires high computational resources for large and complex systems having components with multiple operational states. As a complimentary approach, we propose to use Higher-order-logic (HOL) theorem proving to develop a sound reasoning framework to analyze the reliability of multistate coherent systems in this paper. This framework allows us to formally verify generic mathematical properties about multistate coherent systems with an arbitrary number of components and their states. Particularly, we present the HOL formalization of series and parallel multistate coherent systems and formally verify their deterministic and probabilistic properties using the HOL4 theorem prover. For illustration purposes, we present the formal reliability analysis of the multistate oil and gas pipeline to demonstrate the effectiveness of our proposed framework.

cs.LO↗

arXiv2021

Formalization of Bond Graph using Higher-order-logic Theorem Proving

Bond graph is a unified graphical approach for describing the dynamics of complex engineering and physical systems and is widely adopted in a variety of domains, such as, electrical, mechanical, medical, thermal and fluid mechanics. Traditionally, these dynamics are analyzed using paper-and-pencil proof methods and computer-based techniques. However, both of these techniques suffer from their inherent limitations, such as human-error proneness, approximations of results and enormous computational requirements. Thus, these techniques cannot be trusted for performing the bond graph based dynamical analysis of systems from the safety-critical domains like robotics and medicine. Formal methods, in particular, higher-order-logic theorem proving, can overcome the shortcomings of these traditional methods and provide an accurate analysis of these systems. It has been widely used for analyzing the dynamics of engineering and physical systems. In this paper, we propose to use higher-order-logic theorem proving for performing the bond graph based analysis of the physical systems. In particular, we provide formalization of bond graph, which mainly includes functions that allow conversion of a bond graph to its corresponding mathematical model (state-space model) and the verification of its various properties, such as, stability. To illustrate the practical effectiveness of our proposed approach, we present the formal stability analysis of a prosthetic mechatronic hand using HOL Light theorem prover. Moreover, to help non-experts in HOL, we encode our formally verified stability theorems in MATLAB to perform the stability analysis of an anthropomorphic prosthetic mechatronic hand.

cs.LO↗

arXiv2021

BioNetExplorer: Architecture-Space Exploration of Bio-Signal Processing Deep Neural Networks for Wearables

In this work, we propose the BioNetExplorer framework to systematically generate and explore multiple DNN architectures for bio-signal processing in wearables. Our framework adapts key neural architecture parameters to search for an embedded DNN with a low hardware overhead, which can be deployed in wearable edge devices to analyse the bio-signal data and to extract the relevant information, such as arrhythmia and seizure. Our framework also enables hardware-aware DNN architecture search using genetic algorithms by imposing user requirements and hardware constraints (storage, FLOPs, etc.) during the exploration stage, thereby limiting the number of networks explored. Moreover, BioNetExplorer can also be used to search for DNNs based on the user-required output classes; for instance, a user might require a specific output class due to genetic predisposition or a pre-existing heart condition. The use of genetic algorithms reduces the exploration time, on average, by 9x, compared to exhaustive exploration. We are successful in identifying Pareto-optimal designs, which can reduce the storage overhead of the DNN by ~30MB for a quality loss of less than 0.5%. To enable low-cost embedded DNNs, BioNetExplorer also employs different model compression techniques to further reduce the storage overhead of the network by up to 53x for a quality loss of <0.2%.

eess.SP↗

arXiv2021

ForASec: Formal Analysis of Security Vulnerabilities in Sequential Circuits

Security vulnerability analysis of Integrated Circuits using conventional design-time validation and verification techniques (like simulations, emulations, etc.) is generally a computationally intensive task and incomplete by nature, especially under limited resources and time constraints. To overcome this limitation, we propose a novel methodology based on model checking to formally analyze security vulnerabilities in sequential circuits while considering side-channel parameters like propagation delay, switching power, and leakage power. In particular, we present a novel algorithm to efficiently partition the state-space into corresponding smaller state-spaces to enable distributed security analysis of complex sequential circuits and thereby mitigating the associated state-space explosion due to their feedback loops. We analyze multiple ISCAS89 and trust-hub benchmarks to demonstrate the efficacy of our framework in identifying security vulnerabilities. The experimental results show that ForASec successfully performs the complete analysis of the given complex and large sequential circuits, and provides approximately 11x to 16x speedup in analysis time compared to state-of-the-art model checking-based techniques. Moreover, it also identifies the number of gates required by an HT that can go undetected for a given design and variability conditions.

cs.CR↗

arXiv2020

m2caiSeg: Semantic Segmentation of Laparoscopic Images using Convolutional Neural Networks

Autonomous surgical procedures, in particular minimal invasive surgeries, are the next frontier for Artificial Intelligence research. However, the existing challenges include precise identification of the human anatomy and the surgical settings, and modeling the environment for training of an autonomous agent. To address the identification of human anatomy and the surgical settings, we propose a deep learning based semantic segmentation algorithm to identify and label the tissues and organs in the endoscopic video feed of the human torso region. We present an annotated dataset, m2caiSeg, created from endoscopic video feeds of real-world surgical procedures. Overall, the data consists of 307 images, each of which is annotated for the organs and different surgical instruments present in the scene. We propose and train a deep convolutional neural network for the semantic segmentation task. To cater for the low quantity of annotated data, we use unsupervised pre-training and data augmentation. The trained model is evaluated on an independent test set of the proposed dataset. We obtained a F1 score of 0.33 while using all the labeled categories for the semantic segmentation task. Secondly, we labeled all instruments into an 'Instruments' superclass to evaluate the model's performance on discerning the various organs and obtained a F1 score of 0.57. We propose a new dataset and a deep learning method for pixel level identification of various organs and instruments in a endoscopic surgical scene. Surgical scene understanding is one of the first steps towards automating surgical procedures.

cs.CV↗

arXiv2020

MacLeR: Machine Learning-based Run-Time Hardware Trojan Detection in Resource-Constrained IoT Edge Devices

Traditional learning-based approaches for run-time Hardware Trojan detection require complex and expensive on-chip data acquisition frameworks and thus incur high area and power overhead. To address these challenges, we propose to leverage the power correlation between the executing instructions of a microprocessor to establish a machine learning-based run-time Hardware Trojan (HT) detection framework, called MacLeR. To reduce the overhead of data acquisition, we propose a single power-port current acquisition block using current sensors in time-division multiplexing, which increases accuracy while incurring reduced area overhead. We have implemented a practical solution by analyzing multiple HT benchmarks inserted in the RTL of a system-on-chip (SoC) consisting of four LEON3 processors integrated with other IPs like vga_lcd, RSA, AES, Ethernet, and memory controllers. Our experimental results show that compared to state-of-the-art HT detection techniques, MacLeR achieves 10\% better HT detection accuracy (i.e., 96.256%) while incurring a 7x reduction in area and power overhead (i.e., 0.025% of the area of the SoC and <0.07% of the power of the SoC). In addition, we also analyze the impact of process variation and aging on the extracted power profiles and the HT detection accuracy of MacLeR. Our analysis shows that variations in fine-grained power profiles due to the HTs are significantly higher compared to the variations in fine-grained power profiles caused by the process variations (PV) and aging effects. Moreover, our analysis demonstrates that, on average, the HT detection accuracy drop in MacLeR is less than 1% and 9% when considering only PV and PV with worst-case aging, respectively, which is ~10x less than in the case of the state-of-the-art ML-based HT detection technique.

cs.CR↗

arXiv2020

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.

cs.CR↗

arXiv2020

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.

cs.LG↗

arXiv2020

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.

cs.LO↗

arXiv2020

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.

eess.SP↗