A quantitative metric temporal logic for execution-time constrained verification

Link:
Autor/in:
Verlag/Körperschaft:
Hamburg University of Technology
Erscheinungsjahr:
2019
Medientyp:
Text
Schlagworte:
  • 004: Informatik
  • 600: Technik
  • 610: Medizin
Beschreibung:
  • In the context of run-time model checking, it could be desirable to prioritize and schedule the verification of system properties, so that the verification process, too, meets the time constraints of the underlying online experiment. In this paper, we introduce the Quantitative Metric Temporal Logic for Verification Time (QMTL-VT) to formally describe these constraints on verification time for properties formulated in a given temporal logic. Using QMTL-VT, we can query for satisfaction of time constraints (V), the bounds of execution times (VI), and the probability of being checkable within these bounds (VP). Building up on that, we can execute queries under temporal conditions (VC), express their order (VS), and provide alternatives (VA) for the case of constraint violations. We apply a tool implementation of QMTL-VT to a set of UPPAAL sample models to demonstrate how to perform verification of given properties under real-time constraints, and discuss syntax and semantics in a medical case study on heart-motion tracking as an online real-time scenario.
Beziehungen:
DOI 10.1007/978-3-030-23703-5_9
Quellsystem:
TUHH Open Research

Interne Metadaten
Quelldatensatz
oai:tore.tuhh.de:11420/3080