A Static Checker for Reference Tracking Systems via Laplace Transform and Transfer Functions
Zheng Cheng, Méry, Dominique · HAL (Le Centre pour la Communication Scientifique Directe) · 2023
We propose a static checker, based on the Laplace transform, for checking reference tracking system designs against their performance and safety requirements. It aims to filter out designs that have obvious requirement violations. This is to prevent users from performing more expensive evaluation tasks (e.g., simulation, model checking, or theorem proving) until those violations are reviewed or fixed. In the process, our checker depends on domain knowledge of the Laplace transform to represent each design into a mathematical model, namely the transfer function. Then, it derives time-domain metrics and interprets them as first-order formulas over real numbers. By doing so, we can formulate a proof obligation for checking requirement violations of a design in the Z3 SMT solver. We evaluated our approach on 10 designs from the literature and textbooks to demonstrate its practical usage and identify its limitations.