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

EasyChair Preprint 8009

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

@booklet{EasyChair:8009,
  author    = {Muhammad Ahmed and Adnan Rashid},
  title     = {Formalization of Transform Methods in Higher-Order Logic: a Survey},
  howpublished = {EasyChair Preprint 8009},
  year      = {EasyChair, 2022}}