System analysis based on difference or recurrence equations is 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 paper, 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 and scaling 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. © 2014 Springer International Publishing.
CITATION STYLE
Siddique, U., Mahmoud, M. Y., & Tahar, S. (2014). On the formalization of Z-transform in HOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8558 LNCS, pp. 483–498). Springer Verlag. https://doi.org/10.1007/978-3-319-08970-6_31
Mendeley helps you to discover research relevant for your work.