Most of the engineering and physical systems are generally characterized by diferential and diference 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 diferential/diference 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.
The engineering and physical systems exhibiting dynamical behaviours are generally modeled
using diferential [
The continuous-time dynamical behaviour of a system is generally modeled using diferential equations. These diferential equations-based models are not easier to analyze in time-domain, especially, for the case of larger systems (-order diferential equations for larger ). Transform methods, which include the Laplace and the Fourier transforms have been widely used to
Continuoustime Input Discretetime Input Differential Equation (Continuous) Solving Solution Solution
Solving Difference Equation (Discrete) Laplace Transform Fourier Transform
Inverse Transform Inverse Transform
ZTransform
DF Transform
Laplace form
F(s) Fourier form
F(w)
Solving Solution Solution
Solving Z Form
F(z) DF form
F(w)
Simplification of the expressions Simplification of the expressions Simplification of the expressions Simplification of the expressions
X(s)
System
Y(s) Transfer function = Y(s)/X(s) X(w)
System
Y(w) Frequency response = Y(w)/X(w) X(z)
System
Y(z) Transfer function = Y(z)/X(z) X(w)
System
Y(w)
Frequency response = Y(w)/X(w)
analyze these diferential equations. These methods involve a transformation of the
timedomain model to its corresponding frequency domain representation (-domain for the Laplace
and -domain for the Fourier transform), which converts the diferential equations involving
integrals and diferentials to their corresponding algebraic equations having multiplication
and division operators, as shown in Figure 1. These equations are further solved to analyze
various properties of the system, such as, transfer function and frequency response, and to
obtain solutions in frequency domain [
Similarly, the dynamics of a discrete-time system are captured using diference equations.
These diference equations based models are analyzed using the discrete-time transform methods,
which include the Discrete Fourier Transform (DFT) and the -transform. These transform
methods perform a conversion of the discrete time model to its corresponding frequency domain
representation (-domain for the -transform and for the DFT), as shown in Figure 1. These
representations are further solved to analyze various properties of the given system, such as,
transfer function and frequency response, and to obtain solutions in frequency domain [
Conventionally, the transform methods based analysis has been performed using
paperand-pencil based proofs and computer based symbolic and numerical techniques. However,
these methods sufer from their inherent limitations and thus compromise the accuracy of
the analysis [
The rest of the paper is organized as follows: Section 2 provides the developments of the
Laplace and the Fourier transforms in various theorem provers and their associated analysis of
the continuous-time systems. We provide the formalization of the DFT and the -transform and
the associated analysis of the discrete-time systems in Section 3. Section 4 presents a discussion
about the features and availability of the transform methods based analysis and its comparison
in diferent theorem provers. Finally, Section 5 concludes the paper.
2. Transform Methods for Analyzing Continuous-time Systems
The Laplace and the Fourier transforms have been formalized using various higher-order-logic
theorem provers. Moreover, these formalizations have been used for formally analyzing many
engineering and physical systems. Taqdees et al. [
Wang et al. [21] provided a formalization of the Laplace transform using the Coq theorem prover. The authors formally defined the Laplace transform and formally verified a few of its classical properties, such as, linearity, frequency shifting and diferentiation in time domain. Moreover, they applied their proposed formalization for formally verifying a flight control system using Coq. Similarly, Immler [22] formalized the Laplace transform using the Isabelle theorem prover. The authors mainly verified some of the classical properties of the Laplace transform, such as, linearity, frequency shifting, uniqueness, diferentiation and integration in time-domain. Gang et al. [23] used HOL4 for the formalization of the Laplace transform. The authors formally modeled the Laplace transform and verified some of its classical properties, such as, linearity, frequency shifting, diferentiation and integration in time domain. Next, they used their proposed formalization for formally verifying the transfer function of a motor.
Rashid et al. [26] formalized the Fourier transform using the HOL Light theorem prover. The authors provided a formal definition of the Fourier transform and formally verified its various classical properties, such as, linearity, frequency shifting, modulation, time reversal, ifrst-order and higher-order diefrentiations in time-domain. Furthermore, they formally veriifed the Fourier transform of some commonly used functions, such as, exponential, sine and cosine functions. Moreover, they used their proposed formalization for formally analyzing an Automobile Suspension System (ASS), an audio equalizer, a drug therapy model and a MEMs accelerometer [24]. Similarly, Guan et al. [25] formalized the Fourier transform using HOL4. The authors provided a formal definition of the Fourier transform and formally verified its various properties, such as, linearity, time reversal, frequency shifting, diferentiation and integration in time domain. Moreover, they used their proposed formalization for formally verifying the frequency response of a RLC circuit. A summary of the formalizations of the Laplace and the Fourier transforms in various theorem provers and the systems that have been formally analyzed using these transform methods can be found in Tables 1 and 2. 3. Transform Methods for Analyzing Discrete-time Systems The DFT and -Transform have been formalized using various higher-order-logic theorem provers. Moreover, these formalizations have been used for formally analyzing many discretetime systems. Siddique et al. [27] formalized -transform using the HOL Light theorem prover. The authors provided a formal definition of the -transform and formally verified its various properties, such as, linearity, time shifting and scaling in -domain. Moreover, they used their proposed formalization for the formal analysis of Infinite Impulse Response (IIR) Digital Signal Processing (DSP) filter. Later, the authors extended their proposed framework by providing the formal verification of some more properties, such as, time scaling, complex conjugate and a formal support for the inverse z-transform and used it for formally analyzing a switchedcapacitor interleaved DC-DC voltage doubler [28]. Shi et al. [29] proposed a formalization of DFT using the HOL4 theorem prover. The authors presented a formal definition of the DFT and formally verified its various properties, such as, implicit periodicity, linearity, symmetry, frequency shifting, time sifting and convolution. Moreover, the authors used their proposed formalization for formally verifying Fast Fourier Transform (FFT) and cosine frequency shifting. Capretta et al. [31] formally verified the FFT using the Coq theorem prover. Similarly, Akbarpour et al. [30] provided a formal specification and verification of the FFT at diferent abstraction levels using the HOL4 theorem prover. A summary of the formalization of the transform methods for discrete-time systems in various theorem provers and their associated applications can be found in Tables 3 and 4. 4. Theorem Proving Support for Transform Methods based
Analysis
Transform methods are widely used for analyzing the engineering and physical systems exhibiting dynamical behaviours. Due to the safety-critical nature of these system, their accurate analysis is of utmost importance. This paper surveys the transform methods that have been formalized using diferent theorem provers by highlighting various safety-critical systems that have been formally analyzed based on transform methods. In this regard, only HOL Light theorem prover contains most number of transform methods, such as, the Laplace and the Fourier transforms, and the -transform. Similarly, PVS contains no transform methods library and we need to develop these libraries that can be used for performing transform methods based analysis using PVS. [15] S. H. Taqdees, O. Hasan, Formally Verifying Transfer Functions of Linear Analog Circuits,
IEEE Design & Test 34 (2017) 30–37. [16] A. Rashid, O. Hasan, Formal Analysis of Linear Control Systems using Theorem Proving, in: Formal Engineering Methods, Springer, 2017, pp. 345–361. [17] A. Rashid, O. Hasan, Formalization of Lerch’s Theorem using HOL Light, Journal of
Applied Logics 5 (2018) 1623–1652. [18] S. Abed, A. Rashid, O. Hasan, Formal Analysis of Unmanned Aerial Vehicles Using Higher-Order-Logic Theorem Proving, Journal of Aerospace Information Systems 17 (2020) 481–495. [19] S. Abed, A. Rashid, O. Hasan, Formal Analysis of the Biological Circuits using Higherorder-logic Theorem Proving, in: ACM Symposium on Applied Computing, 2020, pp. 3–7. [20] A. Rashid, O. Hasan, et al., Formal Reasoning about Synthetic Biology using Higher-orderlogic Theorem Proving, IET Systems Biology 14 (2020) 271–283. [21] Y. Wang, G. Chen, Formalization of Laplace Transform in Coq, in: Dependable Systems and Their Applications, IEEE, 2017, pp. 13–21. [22] F. Immler, Laplace Transform (2021). [23] Z. Gang, Z. Chun-na, G. Yong, L. Xing-li, L. Xiao-juan, Formalization of Laplace Transform
Calculus in HOL4, Journal of Chinese Computer Systems 35 (2014) 2177–2181. [24] A. Rashid, O. Hasan, Formal Analysis of Continuous-time Systems using Fourier Transform,
Journal of Symbolic Computation 90 (2019) 65–88. [25] Y. Guan, J. Zhang, Z. Shi, Y. Wang, Y. Li, Formalization of Continuous Fourier Transform in Verifying Applications for Dependable Cyber-physical Systems, Journal of Systems Architecture 106 (2020) 101707. [26] A. Rashid, O. Hasan, On the Formalization of Fourier Transform in Higher-order Logic, in: Interactive Theorem Proving, volume 9807 of LNCS, Springer, 2016, pp. 483–490. [27] U. Siddique, M. Y. Mahmoud, S. Tahar, On the Formalization of -Transform in HOL, in:
Interactive Theorem Proving, volume 8558 of LNCS, Springer, 2014, pp. 483–498. [28] U. Siddique, M. Y. Mahmoud, S. Tahar, Formal Analysis of Discrete-Time Systems using -Transform, Journal of Applied Logics 5 (2018) 875–906. [29] Z. Shi, Y. Zhang, Y. Guan, L. Li, J. Zhang, The Formalization of Discrete Fourier Transform in HOL, Mathematical Problems in Engineering 2015 (2015). [30] B. Akbarpour, S. Tahar, Verification of the Fast Fourier Transform using HOL Theorem
Proving, Techincal Report, Concordia University, Montreal-Canada (2004). [31] V. Capretta, Certifying the Fast Fourier Transform with Coq, in: Theorem Proving in Higher Order Logics, volume 2152 of LNCS, Springer, 2001, pp. 154–168.