| Autor: |
Cheng, Zheng, Méry, Dominique |
| Přispěvatelé: |
Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), TELECOM Nancy, Université de Lorraine (UL), ANR-17-CE25-0005,DISCONT,Intégration correcte de modèles discrets et continus(2017) |
| Jazyk: |
angličtina |
| Rok vydání: |
2023 |
| Předmět: |
|
| Popis: |
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. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
