@article{deniz2024formaltele,
    title={Formalization of the Telegrapher's Equations using Higher-Order-Logic Theorem Proving},
    author={Deniz, Elif and Rashid, Adnan and Hasan, Osman and Tahar, Sofiene},
    journal={Journal of Applied Logics - IfCoLog Journal},
    volume={11},
    number={2},
    pages={197-236},
    year={2024},
    publisher={College Publications}
  }

The telegrapher’s equations constitute a set of linear partial differential equations that establish a mathematical correspondence between the electrical current and voltage within transmission lines, taking into account factors, such as distance and time. These equations find wide applications in the design and analysis of various systems, including integrated circuits and antennas. This paper proposes the utilization of higher-order-logic theorem proving for a formal analysis of the telegrapher’s equations, also referred to as the transmission line equations. Specifically, we present a formal model of the telegrapher’s equations in both time and phasor domains. Subsequently, we employ the HOL Light theorem prover to formally verify the solutions of the telegrapher’s equations in the phasor domain. Furthermore, we established a connection between phasor and time-domain functions to formally verify the general solutions for the time-domain partial differential equations for the current and voltage in an electric transmission line. To demonstrate the practical effectiveness of our proposed formalization, we conduct a formal analysis of a terminated transmission line and its special cases, i.e., short and open-circuited transmission lines commonly used in antenna design, by formally verifying the load impedance and the voltage reflection coefficient.

@article{rashid2022formal,
    title={{Formal Analysis of 2D Image Processing Filters using Higher-order-logic Theorem Proving}},
    author={Rashid, Adnan and Abed, Sa’ed and Hasan, Osman},
    journal={EURASIP Journal on Advances in Signal Processing},
    volume={1},
    number={53},
    pages={1-18},
    year={2022},
    publisher={Springer}
  }

Two-dimensional (2D) image processing systems are concerned with the processing of the images represented as 2D arrays and are widely used in medicine, transportation and many other autonomous systems. The dynamics of these systems are generally modeled using 2D difference equations, which are mathematically analyzed using the 2D z-transform. It mainly involves a transformation of the difference equations-based models of these systems to their corresponding algebraic equations, mapping the 2D arrays (2D discrete-time signals) over the (z1,z2)-domain. Finally, these (z1,z2)-domain representations are used to analyze various properties of these systems, such as transfer function and stability. Conventional techniques, such as paper-and-pencil proof methods, and computer-based simulation techniques for analyzing these filters cannot assert the accuracy of the analysis due to their inherent limitations like human error proneness, limited computational resources and approximations of the mathematical expressions and results. In this paper, as a complimentary technique, we propose to use formal methods, higher-order logic (HOL) theorem proving, for formally analyzing the image processing filters. These methods can overcome the limitations of the conventional techniques and thus ascertain the accuracy of the analysis. In particular, we formalize the 2D z-transform based on the multivariate theories of calculus using the HOL Light theorem prover. Moreover, we formally analyze a generic (L1,L2)-order 2D infinite impulse response image processing filter. We illustrate the practical effectiveness of our proposed approach by formally analyzing a second-order image processing filter.

@article{murtza2023towards,
    title={{Towards the Formal Performance Analysis of Multistate Coherent Systems using HOL Theorem Proving}},
    author={Murtza, Shahid Ali and Ahmed, Waqar and Rashid, Adnan and Hasan, Osman},
    journal={Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability},
    volume={237},
    number={1},
    pages={180--194},
    year={2023},
    publisher={SAGE Publications Sage UK: London, England}
  }  

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.

@article{qasim2022formalization,
    title={{Formalization of Bond Graph using Higher-order-logic Theorem Proving}},
    author={Qasim, Ujala and Rashid, Adnan and Hasan, Osman},
    journal={ISA transactions},
    volume={128},
    pages={453--469},
    year={2022},
    publisher={Elsevier}
  }  

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.

@article{gauhar2021formal,
    title={{Formal Verification of Matrix based MATLAB Models using Interactive Theorem Proving}},
    author={Gauhar, Ayesha and Rashid, Adnan and Hasan, Osman and Bispo, Jo{\~a}o and Cardoso, Jo{\~a}o MP},
    journal={PeerJ Computer Science},
    volume={7},
    pages={e440},
    year={2021},
    publisher={PeerJ Inc.}
  }  

MATLAB is a software based analysis environment that supports a high-level programing language and is widely used to model and analyze systems in various domains of engineering and sciences. Traditionally, the analysis of MATLAB models is done using simulation and debugging/testing frameworks. These methods provide limited coverage due to their inherent incompleteness. Formal verification can overcome these limitations, but developing the formal models of the underlying MATLAB models is a very challenging and time-consuming task, especially in the case of higher-order-logic models. To facilitate this process, we present a library of higher-order-logic functions corresponding to the commonly used matrix functions of MATLAB as well as a translator that allows automatic conversion of MATLAB models to higher-order logic. The formal models can then be formally verified in an interactive theorem prover. For illustrating the usefulness of the proposed library and approach, we present the formal analysis of a Finite Impulse Response (FIR) filter, which is quite commonly used in digital signal processing applications, within the sound core of the HOL Light theorem prover.

@article{rashid2021formal,
    title={{Formal Analysis of the Continuous Dynamics of Cyber-physical Systems using Theorem Proving}},
    author={Rashid, Adnan and Hasan, Osman},
    journal={Journal of Systems Architecture},
    volume={112},
    pages={101850},
    year={2021},
    publisher={Elsevier}
  }  

Transform methods, such as the Laplace and the Fourier transforms, are widely used for analyzing the continuous dynamics of the physical components of Cyber–physical Systems (CPS). Traditionally, the transform methods based analysis of CPS is conducted using paper-and-pencil proof methods, computer-based simulations or computer algebra systems. However, all these methods cannot capture the continuous aspects of physical systems in their true form and thus unable to provide a complete analysis, which poses a serious threat to the safety of CPS. To overcome these limitations, we propose to use higher-order-logic theorem proving to reason about the dynamical behavior of CPS, based on the Laplace and the Fourier transforms, which ensures the absolute accuracy of this analysis. For this purpose, this paper presents a higher-order-logic formalization of the Laplace and the Fourier transforms, including the verification of their classical properties and uniqueness. This formalization plays a vital role in formally verifying the solutions of differential equations in both the time and the frequency domain and thus facilitates formal dynamical analysis of CPS. For illustration, we formally analyze an industrial robot and an equalizer using the HOL Light theorem prover.

@article{abed2020formal,
    title={{Formal Reasoning about Synthetic Biology using Higher-order-logic Theorem Proving}},
    author={Abed, Sa'ed and Rashid, Adnan and Hasan, Osman},
    journal={IET Systems Biology},
    volume={14},
    number={5},
    pages={271--283},
    year={2020},
    publisher={Wiley Online Library}
  }  

Synthetic biology is an interdisciplinary field that uses well-established engineering principles for performing the analysis of the biological systems, such as biological circuits, pathways, controllers and enzymes. Conventionally, the analysis of these biological systems is performed using paper-and-pencil proofs and computer simulation methods. However, these methods cannot ensure accurate results due to their inherent limitations. Higher-order-logic (HOL) theorem proving is proposed and used as a complementary approach for analysing linear biological systems, which is based on developing a mathematical model of the genetic circuits and the bio-controllers used in synthetic biology based on HOL and analysing it using deductive reasoning in an interactive theorem prover. The involvement of the logic, mathematics and the deductive reasoning in this method ensures the accuracy of the analysis. It is proposed to model the continuous dynamics of the genetic circuits and their associated controllers using differential equations and perform their transfer function-based analysis using the Laplace transform in a theorem prover. For illustration, the genetic circuits of activated and repressed expressions and autoactivation of protein, and phase lag and lead controllers, which are widely used in cancer-cell identifiers and multi-input receptors for precise disease detection, are formally analyzed.

@article{rashid2020formal,
    title={{Formal Verification of Robotic Cell Injection Systems up to 4-DOF using HOL Light}},
    author={Rashid, Adnan and Hasan, Osman},
    journal={Formal Aspects of Computing},
    volume={32},
    pages={229--250},
    year={2020},
    publisher={Springer}
  }  

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 and in-vitro fertilization. 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 obtained by controlling the orientation and movement of its various components, like injection manipulator, microscope etc., and planning the motion of the injection pipette by controlling the force of the injection. The conventional techniques to analyze the cell injection process include paper-and-pencil proof and computer simulation methods. However, both these techniques suffer from their inherent limitations, such as, proneness to human error for the former and the approximation of the mathematical expressions involved in the numerical algorithms for the latter. Formal methods have the capability to overcome these limitations and can provide an accurate analysis of these cell injection systems. Model checking, i.e., a state-based formal method, has been recently used for analyzing these systems. However, it involves the discretization of the differential equations capturing the continuous dynamics of the system and thus compromises on the completeness of the analysis of these safety-critical systems. In this paper, we propose a higher-order-logic theorem proving (a deductive-reasoning based formal method) based framework for analyzing the dynamical behavior of the robotic cell injection systems upto 4-DOF. 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.

@article{abed2020formal,
    title={{Formal Analysis of Unmanned Aerial Vehicles using Higher-order-logic Theorem Proving},
    author={Abed, Sa’ed and Rashid, Adnan and Hasan, Osman},
    journal={Journal of Aerospace Information Systems},
    volume={17},
    number={9},
    pages={481--495},
    year={2020},
    publisher={American Institute of Aeronautics and Astronautics}
  }  

The continuous dynamics of unmanned aerial vehicles (UAVs) are generally modeled as a set of differential equations. Traditionally, these continuous dynamics of UAVs are analyzed using paper-and-pencil proof and computer-based testing or simulations to study the performance, stability, and various other control characteristics of the aircraft flying in the air. However, these techniques suffer from their inherent limitations such as human error proneness, sampling-based analysis, approximations of the mathematical results, and the usage of unverified algorithms. Thus, these methods cannot be trusted when considering the utility of UAVs in many safety-critical applications. To overcome the limitations of the aforementioned techniques, it is proposed to use higher-order-logic theorem proving for formally analyzing the continuous dynamics of UAVs. In particular, a formalization of complex-valued matrices in higher-order logic is provided using the HOL Light theorem prover, which is in turn used for the formalization of the navigation’s and aircraft’s body-fixed frames, as well as their associated transformations. Formal reasoning support is also provided for analyzing the multiple-input multiple-output systems, which are in turn used for formally analyzing the continuous dynamics of UAVs using HOL Light. For illustration, we use our proposed framework for the formal stability analysis of the CropCam UAV using HOL Light.

@article{rashid2020toward,
    title={Toward the formalization of macroscopic models of traffic flow using higher-order-logic theorem proving},
    author={Rashid, Adnan and Umair, Muhammad and Hasan, Osman and Zaki, Mohamed H},
    journal={IEEE Access},
    volume={8},
    pages={27291--27307},
    year={2020},
    publisher={IEEE}
  }  

Next-generation transportation will be integrated, interconnected and highly autonomous. One key challenge in traffic management is ensuring safety while maintaining the required level of service quality. In such future mobility systems, rigorous formalization and validation will thus become critical to ensure that the transportation network operates as intended, traffic properties are reliably maintained, and services resume in a timely manner after potential disruptions. Formal methods have recently gained considerable attention as a modeling and verification paradigm capable of addressing many challenges associated with next-generation transportation systems. In this regard, we propose to use higher-order-logic theorem proving for formally analyzing transportation systems. As a first step towards this direction, we present a logical framework for the formal analysis of macroscopic models of traffic flow. Leveraging upon the high expressiveness of the underlying logic, we formally model the continuous components of macroscopic models while capturing their real behavior. In particular, we present a formalization of some foundation concepts of macroscopic models, namely density, flow rate, mean speed, relative occupancy, and shockwave using the higher-order-logic theorem prover HOL Light. This choice is primarily motivated by the fact that the macroscopic models deal with the traffic flow dynamics and thus play a vital role in planning strategies in allocating resources for implementing optimized and balanced transportation systems. For illustration, we perform the formal input-output and shockwave analysis of a German freeway. The case study demonstrated the practicability of this formal approach due to the high expressiveness of the underlying logic. The proposed research is first step towards formalizing the foundational mathematical theories and core concepts of traffic flow theory. This accomplishment will open new ways to plan and model various components of the transportation systems such as highway links, ramp metering, merging behavior and eventually address the problem of routing vehicles in a network of automated vehicles.

@article{hasan2017formal,
    title={Formal analysis of continuous-time systems using fourier transform},
    author={Hasan, O},
    journal={Journal of symbolic computation},
    year={2017}
  }  

To study the dynamical behavior of the engineering and physical systems, we often need to capture their continuous behavior, 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.

@article{rashid2018formalization,
    title={Formalization of Lerch’s Theorem using HOL Light},
    author={Rashid, Adnan and Hasan, Osman},
    journal={Journal of Applied Logics},
    volume={5},
    number={8},
    pages={1623},
    year={2018}
  }  

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).

@article{rashid2019wearable,
    title={Wearable technologies for hand joints monitoring for rehabilitation: A survey},
    author={Rashid, Adnan and Hasan, Osman},
    journal={Microelectronics Journal},
    volume={88},
    pages={173--183},
    year={2019},
    publisher={Elsevier}
  }  

Hand deformities often become a major obstacle in conducting everyday tasks for many people around the globe. Rehabilitation procedures are widely used for strengthening the hand muscles, which in turn leads to the restoration of functionality of the affected hand. This paper conducts a survey of various wearable technologies that can be used to accurately quantify the rehabilitation progress in terms of fingers' hand joint angles. Based on the data acquisition methods, these technologies can be mainly divided into six categories: 1) Flex sensor based; 2) Accelerometer based; 3) Vision based; 4) Hall-effect based; 5) Stretch sensor based; and 6) Magnetic sensor based. The main focus of some of the discussed technologies has been on various other domains, like gaming gloves, tele-manipulation etc., and thus their usage for rehabilitation of hand joints could be quite interesting. This paper analyzes the strengths and weaknesses of these wearable technologies along with some examples of their implementations. Based on our survey results, we propose a wearable glove for accurately measuring hand joint angles with enhanced features for better diagnosis and rehabilitation.

@article{rashid2017formal,
    title={Formal reasoning about systems biology using theorem proving},
    author={Rashid, Adnan and Hasan, Osman and Siddique, Umair and Tahar, Sofiene},
    journal={PloS one},
    volume={12},
    number={7},
    pages={e0180179},
    year={2017},
    publisher={Public Library of Science San Francisco, CA USA}
  }  

System biology provides the basis to understand the behavioral properties of complex biological organisms at different levels of abstraction. Traditionally, analysing systems biology based models of various diseases have been carried out by paper-and-pencil based proofs and simulations. However, these methods cannot provide an accurate analysis, which is a serious drawback for the safety-critical domain of human medicine. In order to overcome these limitations, we propose a framework to formally analyze biological networks and pathways. In particular, we formalize the notion of reaction kinetics in higher-order logic and formally verify some of the commonly used reaction based models of biological networks using the HOL Light theorem prover. Furthermore, we have ported our earlier formalization of Zsyntax, i.e., a deductive language for reasoning about biological networks and pathways, from HOL4 to the HOL Light theorem prover to make it compatible with the above-mentioned formalization of reaction kinetics. To illustrate the usefulness of the proposed framework, we present the formal analysis of three case studies, i.e., the pathway leading to TP53 Phosphorylation, the pathway leading to the death of cancer stem cells and the tumor growth based on cancer stem cells, which is used for the prognosis and future drug designs to treat cancer patients.

@inproceedings{deniz2024abcdpar,
        title={{Formal Verification of ABCD Parameters Based Models for Transmission Lines}},
        author={Deniz, Elif and Rashid, Adnan and Hasan, Osman and Tahar, Sofi{\`e}ne},
        booktitle={International Symposium on Symbolic Computation in Software Science},
        pages={X--Y},
        year={2024},
        organization={Springer}
      }   
    

Formal Verification of ABCD Parameters Based Models for Transmission Lines

@inproceedings{rashid2023formal,
    title={{Formal Stability Analysis of Two-Dimensional Digital Image Processing Filters}},
    author={Rashid, Adnan and Abed, Sa’ed and Hasan, Osman},
    booktitle={International Congress on Information and Communication Technology},
    pages={583--591},
    year={2023},
    organization={Springer}
  }     

There are several image processing applications that require to partition frequency components of images. This requirement is usually fulfilled by using digital image processing filters. Most of this processing is done in two-dimensions given the two-dimensions of the regular images. It is very important to ascertain that these filters provide a stable output for a bounded input, and this requirement is usually termed as stability. The stability analysis of these filters is usually conducted analytically, on a piece of paper, or by simulations. However, these techniques provide approximate or inaccurate results as paper-based analysis can have human error and simulations suffer from computer arithmetic related roundoff limitations. We advocate formally analyzing the stability of digital filters for two-dimensional (2D) images using interactive theorem proving. In this regard, we present a formal dynamical model and a formal notion of stability of 2D digital image processing filters in HOL Light. The proposed formal model is used to perform the stability analysis of a real-world 2nd-order filter in HOL Light.

@inproceedings{ali2023anti,
        title={{Anti-social Behavior Detection using Multi-lingual Model}},
        author={Ali, Hafiz Zeeshan and Rashid, Adnan},
        booktitle={International Conference on Advancements in Computational Sciences},
        pages={1--9},
        year={2023},
        organization={IEEE}
      }          
    

In the current era, social media has emerged as a very useful and reliable means of communication between different people and communities. However, with the leverage of communication platforms and billions of social media users, it became more challenging to stop hateful, abusive, or offensive content spread by extremists that are various aspects of Anti-social Behavior (ASB). Multiple users from several regions use different languages (a mix of native, local and other languages) to express their emotions. Roman Urdu-English and Roman Hindi-English are the two most commonly used languages on social media in the South Asia region. Therefore, the ASB detection with multilingual (multiple languages) model settings represents a wide area of interest for all kinds of social media platforms. Failing to properly address this issue over time on a global scale has already led to morally questionable real-life events, human deaths, and the perpetuation of hate itself. In this paper, we perform a sentimental analysis of the Roman Urdu-English and Roman Hindi-English languages using transformer based mBERT and XLM-R models. Moreover, we process the negatively classified sequences for detection of the ASB.

@inproceedings{deniz2022formalization,
        title={On the Formalization of the Heat Conduction Problem in HOL},
        author={Deniz, Elif and Rashid, Adnan and Hasan, Osman and Tahar, Sofi{\`e}ne},
        booktitle={International Conference on Intelligent Computer Mathematics},
        pages={21--37},
        year={2022},
        organization={Springer}
      }   
    

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.

@article{ahmed2021formalization,
    title={Formalization of Transform Methods in Higher-order Logic: A Survey},
    author={Ahmed, Muhammad and Rashid, Adnan},
    journal={arXiv preprint arXiv:2111.10049},
    year={2021}
  }  

Most of the engineering and physical systems are generally characterized by differential and difference equations based on their continuous-time and discrete-time dynamics, respectively. Moreover, these dynamical models are analyzed using transform methods to prove various properties of these systems, such as, transfer function, frequency response and stability, and to find out solutions of the differential/difference equations. The conventional techniques for performing the transform methods based analysis have been unable to provide an accurate analysis of these systems. Therefore, higher-order-logic theorem proving, a formal method, has been used for accurately analyzing systems based on transform methods. In this paper, we survey developments for transform methods based analysis in various higher-order-logic theorem provers and overview the corresponding real world case studies from the avionics, medicine and transportation domains that have been analyzed based on these developments.

@inproceedings{rashid2020fasim,
    title={FASiM: A Framework for Automatic Formal Analysis of Simulink Models of Linear Analog Circuits},
    author={Rashid, Adnan and Gauhar, Ayesha and Hasan, Osman},
    booktitle={2020 IEEE International Systems Conference (SysCon)},
    pages={1--7},
    year={2020},
    organization={IEEE}
  }  

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.

@inproceedings{abed2020formal,
    title={Formal analysis of the biological circuits using higher-order-logic theorem proving},
    author={Abed, Sa'ed and Rashid, Adnan and Hasan, Osman},
    booktitle={Proceedings of the 35th Annual ACM Symposium on Applied Computing},
    pages={3--7},
    year={2020}
  }  

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.

@inproceedings{rashid2020formal,
    title={Formal verification of cyber-physical systems using theorem proving},
    author={Rashid, Adnan and Siddique, Umair and Tahar, Sofi{\`e}ne},
    booktitle={Formal Techniques for Safety-Critical Systems: 7th International Workshop, FTSCS 2019, Shenzhen, China, November 9, 2019, Revised Selected Papers 7},
    pages={3--18},
    year={2020},
    organization={Springer}
  }  

Due to major breakthroughs in software and engineering technologies, embedded systems are increasingly being utilized in areas ranging from aerospace and next-generation transportation systems, to smart grid and smart cities, to health care systems, and broadly speaking to what is known as Cyber-Physical Systems (CPS). A CPS is primarily composed of several electronic, communication and controller modules and some actuators and sensors. The mix of heterogeneous underlying smart technologies poses a number of technical challenges to the design and more severely to the verification of such complex infrastructure. In fact, a CPS shall adhere to strict safety, reliability, performance and security requirements, where one needs to capture both physical and random aspects of the various CPS modules and then analyze their inter-relationship across interlinked continuous and discrete dynamics. Often-times however, system bugs remain uncaught during the analysis and in turn cause unwanted scenarios that may have serious consequences in safety-critical applications. In this paper, we introduce some of the challenges surrounding the design and verification of contemporary CPS with the advent of smart technologies. In particular, we survey recent developments in the use of theorem proving, a formal method, for the modeling, analysis and verification of CPS, and overview some real world CPS case studies from the automotive, avionics and healthtech domains from system level to physical components.

@article{rashid2018formal,
    title={Formal modeling of robotic cell injection systems in higher-order logic},
    author={Rashid, Adnan and Hasan, Osman},
    journal={arXiv preprint arXiv:1807.07378},
    year={2018}
  }  

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.

@inproceedings{rashid2018formal,
    title={Formal verification of platoon control strategies},
    author={Rashid, Adnan and Siddique, Umair and Hasan, Osman},
    booktitle={Software Engineering and Formal Methods: 16th International Conference, SEFM 2018, Held as Part of STAF 2018, Toulouse, France, June 27--29, 2018, Proceedings 16},
    pages={223--238},
    year={2018},
    organization={Springer}
  }  

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.

@inproceedings{rashid2019formal,
    title={Formal analysis of robotic cell injection systems using theorem proving},
    author={Rashid, Adnan and Hasan, Osman},
    booktitle={Cyber Physical Systems. Design, Modeling, and Evaluation: 7th International Workshop, CyPhy 2017, Seoul, South Korea, October 15-20, 2017, Revised Selected Papers 7},
    pages={127--141},
    year={2019},
    organization={Springer}
  }  

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.

@inproceedings{rashid2017formal,
    title={Formal analysis of linear control systems using theorem proving},
    author={Rashid, Adnan and Hasan, Osman},
    booktitle={Formal Methods and Software Engineering: 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi'an, China, November 13-17, 2017, Proceedings},
    pages={345--361},
    year={2017},
    organization={Springer}
  }  

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.

@inproceedings{rashid2017formalization,
    title={Formalization of transform methods using HOL light},
    author={Rashid, Adnan and Hasan, Osman},
    booktitle={Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings 10},
    pages={319--332},
    year={2017},
    organization={Springer}
  }  

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.

@inproceedings{rashid2016formalization,
    title={On the formalization of Fourier transform in higher-order logic},
    author={Rashid, Adnan and Hasan, Osman},
    booktitle={Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings 7},
    pages={483--490},
    year={2016},
    organization={Springer}
  }  

Fourier transform based techniques are widely used for solving differential equations and to perform the frequency response analysis of signals in many safety-critical systems. To perform the formal analysis of these systems, we present a formalization of Fourier transform using higher-order logic. In particular, we use the HOL-Light’s 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, frequency shifting, modulation, time reversal and differentiation in time-domain. In order to demonstrate the practical effectiveness of the proposed formalization, we use it to formally verify the frequency response of an automobile suspension system.

@inproceedings{rashid2015formal,
        title={Formal analysis of a ZigBee-based routing protocol for smart grids using UPPAAL},
        author={Rashid, Adnan and Hasan, Osman and Saghar, Kashif},
        booktitle={2015 12th International Conference on High-capacity Optical Networks and Enabling/Emerging Technologies (HONET)},
        pages={1--5},
        year={2015},
        organization={IEEE}
      }  
    

Smart grid is an emerging technology which integrates the modern communication network to the traditional power grids. The performance and efficiency of the smart grid mainly depends on reliable communication between its different components and in turn on the routing protocols that establish this communication network. ZigBee protocol is a widely used routing protocol in the home area networks of the smart grids. Traditionally, these protocols are analysed using computer simulations and net testing. All these methods are error-prone and thus cannot provide an accurate analysis, which poses a serious threat to the safety-critical domain of smart grids. To guarantee the correctness of analysis, we propose to use model checking for the verification of the ZigBee routing protocol. We used UPPAAL model checker to formally model the ZigBee routing protocol and verified it using the collision avoidance and liveness properties.

@inproceedings{ahmed2014analysis,
    title={Analysis of weather forecasting model in PRISM},
    author={Ahmed, Asad and Rashid, Adnan and Iqbal, Sohail},
    booktitle={2014 12th International Conference on Frontiers of Information Technology},
    pages={355--360},
    year={2014},
    organization={IEEE}
  }  

Weather forecasting provides an important information for general public. Analysis of weather forecasting models, through traditional simulation techniques, are not exhaustive and thus not accurate. Probabilistic model checking, a formal methods technique, as a complementary approach provides an accurate analysis for probabilistic models. In this paper, we have analyzed a simple probabilistic weather forecasting model for Islamabad weather using PRISM model checker. The reach ability and prediction capability of model has been analyzed using quantitative and qualitative properties in PRISM. Analysis shows that all the states of weather forecasting model are reachable and model is biased. In addition, we have also implemented this model in MATLAB and compared the results of both implementation, quantitatively. We have also presented a comparison between PRISM and MATLAB implementation of weather forecasting model, qualitatively.