Formal analysis of continuous-time systems using Fourier transform
From MaRDI portal
Abstract: To study the dynamical behaviour of the engineering and physical systems, we often need to capture their continuous behaviour, which is modeled using differential equations, and perform the frequency-domain analysis of these systems. Traditionally, Fourier transform methods are used to perform this frequency domain analysis using paper-and-pencil based analytical techniques or computer simulations. However, both of these methods are error prone and thus are not suitable for analyzing systems used in safety-critical domains, like medicine and transportation. In order to provide an accurate alternative, we propose to use higher-order-logic theorem proving to conduct the frequency domain analysis of these systems. For this purpose, the paper presents a higher-order-logic formalization of Fourier transform using the HOL-Light theorem prover. In particular, we use the higher-order-logic based formalizations of 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, time shifting, frequency shifting, modulation, time scaling, time reversal and differentiation in time domain, and its relationships with Fourier Cosine, Fourier Sine and Laplace transforms. We use our proposed formalization for the formal verification of the frequency response of a generic n-order linear system, an audio equalizer and a MEMs accelerometer, using the HOL-Light theorem prover.
Recommendations
- On the formalization of Fourier transform in higher-order logic
- Formalization of transform methods using HOL Light
- scientific article; zbMATH DE number 7594146
- The formalization of discrete Fourier transform in HOL
- Formalization of Laplace transform using the multivariable calculus theory of HOL-Light
Cites work
- scientific article; zbMATH DE number 5539366 (Why is no real title available?)
- scientific article; zbMATH DE number 3657618 (Why is no real title available?)
- scientific article; zbMATH DE number 3790965 (Why is no real title available?)
- scientific article; zbMATH DE number 1987817 (Why is no real title available?)
- scientific article; zbMATH DE number 958048 (Why is no real title available?)
- Formalization of Laplace transform using the multivariable calculus theory of HOL-Light
- Formalization of transform methods using HOL Light
- Foundations of digital signal processing: theory, algorithms and hardware design. With 1 CD-ROM
- Matlab guide
- On the Formalization of Z-Transform in HOL
- On the formalization of Fourier transform in higher-order logic
- The HOL Light theory of Euclidean space
- The misfortunes of a trio of mathematicians using computer algebra systems. Can we trust in them?
- Understanding Maple
Cited in
(7)- Formalization of Laplace transform using the multivariable calculus theory of HOL-Light
- On the formalization of the heat conduction problem in HOL
- scientific article; zbMATH DE number 3107461 (Why is no real title available?)
- Verified interactive computation of definite integrals
- On the formalization of Fourier transform in higher-order logic
- Formalization of transform methods using HOL Light
- The formalization of discrete Fourier transform in HOL
Describes a project that uses
Uses Software
This page was built for publication: Formal analysis of continuous-time systems using Fourier transform
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1640640)
