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.
CITATION STYLE
Rashid, A., & Hasan, O. (2016). On the formalization of Fourier transform in higher-order logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9807 LNCS, pp. 483–490). Springer Verlag. https://doi.org/10.1007/978-3-319-43144-4_31
Mendeley helps you to discover research relevant for your work.