The computer implementation of a majority of
engineering and physical systems requires the discretization of continuous parameters (e.g., time, temperature, voltage, etc.).
Such systems are then called discrete-time systems and their dynamics can be described by difference or
recurrence equations. Recently, there is an increasing interest in applying formal methods
in the domain of cyber-physical systems to identify subtle but critical design bugs, which can lead to critical failures and
monetary loss. In this paper,
we propose to formally reason about discrete-time systems using the z-Transform, which is
a mathematical tool to transform a time-domain model to a corresponding complex-frequency domain model.
In particular, we present the HOL Light formalization of the z-Transform and
difference equations along with some important properties such as linearity, time-delay and
complex translation. An interesting part of our work is the formal proof of the uniqueness of the z-Transform.
Indeed, the uniqueness of the z-Transform plays a vital role in reliably deducing important properties of complex systems.
We apply our work to formally analyze a switched-capacitor interleaved DC-DC voltage doubler and
an infinite impulse response (IIR) filter, which are important
components of a wide class of power electronics, control and signal processing systems.

## Applications

## Publications

## Source Code

HOL Light Sources

** Switched-Capacitor (SC) Power Converter**

** Infinite Impulse Response (IIR) Filter**

- U. Siddique, M. Y. Mahmoud and S. Tahar:
Formal Analysis of Discrete-Time Systems using z-Transform, Journal of Applied Logic, Vol. 5, No. 4, June 2018, pp. 875-906.

- U. Siddique, M. Y. Mahmoud and S. Tahar:
On the Formalization of Z-Transform in HOL, G. Klein and R. Gamboa (Eds.), Interactive Theorem Proving,Lecture Notes in Computer Science Volume 8558, 2014, pp 483-498.
[Proc. Conference on Interactive Theorem Proving (ITP'14), Vienna, Austria, July 2014]