 Formal Analysis of DiscreteTime Systems using zTransform
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 discretetime 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 cyberphysical 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 discretetime aspects of cyberphysical systems using the $z$Transform, which is a mathematical tool to transform a timedomain model to a corresponding complexfrequency 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, timedelay 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 switchedcapacitor interleaved DCDC 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.
