Download PDFOpen PDF in browserFormalization of Transform Methods in Higher-Order Logic: a SurveyEasyChair Preprint no. 80097 pages•Date: May 22, 2022AbstractMost 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
|