|Formal Analysis of Discrete-Time Systems using z-Transform|
Umair Siddique, Mohamed Yousri Mahmoud and Sofiène Tahar
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 aspects of cyber-physical 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.