A quantitative metric temporal logic for execution-time constrained verification

Publikationstyp
Conference Paper
Date Issued
2019
Sprache
English
Author(s)
Lehmann, Sascha 
Antoni, Sven-Thomas  
Schlaefer, Alexander  
Schupp, Sibylle  
Institut
Softwaresysteme E-16  
Medizintechnische Systeme E-1  
TORE-URI
http://hdl.handle.net/11420/3080
First published in
Lecture notes in computer science  
Number in series
11615 LNCS
Start Page
170
End Page
189
Citation
Lecture Notes in Computer Science (11615 LNCS): 170-189 (2019)
Contribution to Conference
International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems Workshop on Embedded Systems and Cyber-Physical Systems Education, CyPhy 2018, WESE 2018  
Publisher DOI
10.1007/978-3-030-23703-5_9
Scopus ID
2-s2.0-85069171101
Publisher
Springer
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.
DDC Class
004: Informatik
600: Technik
610: Medizin