A Static Checker for Reference Tracking Systems via Laplace Transform and Transfer Functions - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2023

A Static Checker for Reference Tracking Systems via Laplace Transform and Transfer Functions

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (384.17 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-04152829 , version 1 (05-07-2023)

Licence

Copyright (Tous droits réservés)

Identifiants

  • HAL Id : hal-04152829 , version 1

Citer

Zheng Cheng, Dominique Méry. A Static Checker for Reference Tracking Systems via Laplace Transform and Transfer Functions. 2023. ⟨hal-04152829⟩
31 Consultations
26 Téléchargements

Partager

Gmail Facebook X LinkedIn More