Download PDFOpen PDF in browser

Formalization of Transform Methods in Higher-Order Logic: a Survey

EasyChair Preprint no. 8009

7 pagesDate: May 22, 2022

Abstract

Most of the engineering and physical systems are generally characterized by differential equations or difference equations based on their continuous-time and discrete-time dynamics, respectively. Moreover, these dynamical models are analyzed using transform methods to find out solutions of the differential/difference equations and prove their various properties, such as, transfer function, frequency response and stability. The Laplace and the Fourier transforms are used for analyzing systems exhibiting continuous dynamics. Whereas, the Discrete Fourier Transform (DFT) and the z-transform are their counterpart in the discrete time. The conventional techniques for performing the transform methods based analysis cannot provide an accurate analysis of the corresponding systems due to their inherent limitations. To overcome these limitations, formal methods, in particular, theorem proving, has been used, as a complementary technique, for analyzing systems based on transform methods and thus ascertain an accurate analysis. In this paper, we survey the developments in the use of higher-order-logic theorem proving for transform methods based analysis and overview the corresponding real world case studies from the avionics, medicine and transportation domains that have been analyzed based on these developments.

Keyphrases: continuous-time system, differential equation, Discrete Fourier Transform, discrete-time system, formal analysis, formal methods, formalization, Fourier transform, frequency response, higher-order logic, HOL Light, Laplace transform, theorem prover, theorem proving, transfer function, transform method, transform method based analysis, transform methods

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@Booklet{EasyChair:8009,
  author = {Muhammad Ahmed and Adnan Rashid},
  title = {Formalization of Transform Methods in Higher-Order Logic: a Survey},
  howpublished = {EasyChair Preprint no. 8009},

  year = {EasyChair, 2022}}
Download PDFOpen PDF in browser