On the Formalization of Z-Transform in HOL
Contact: muh_sidd@ece.concordia.ca , mo_solim@ece.concordia.ca
Descrition
System analysis based on difference equations or recurrence equations are the most fundamental technique to analyze biological, electronic, control and signal processing systems. Z-transform is one of the most popular tool to solve such difference equations. In this work, we present the formalization of Z-transform to extend the formal linear system analysis capabilities using theorem proving. In particular, we use differential, transcendental and topological theories of multivariate calculus to formally define Z-transform in higher-order logic and reason about the correctness of its properties, such as linearity, time shifting, scaling and differentiation in z-domain. To illustrate the practical effectiveness of the proposed formalization, we present the formal analysis of an infinite impulse response (IIR) digital signal processing filter.Application
Infinite Impulse Response (IIR) Filter:
Digital filters are fundamental components of almost all signal processing and communication systems. An impulse response of a system describes its behaviour under an external change (mathematically, this describes the system response when the dirac-delta function is applied as an input). Infinite impulse response (IIR) filters have an impulse response function which is non-zero over an infinite length of time. Given the filter specifications in terms of frequency response, the first step is to model the filter using constant coefficient difference equations. The next step is to express it in the form of transfer function using the Z-transform properties. Consequently, frequency response analysis and architectural optimization can be performed based on the given specifications.
