Lehmann, SaschaSaschaLehmannAntoni, Sven-ThomasSven-ThomasAntoniSchlaefer, AlexanderAlexanderSchlaeferSchupp, SibylleSibylleSchupp2019-08-092019-08-092019Lecture Notes in Computer Science (11615 LNCS): 170-189 (2019)http://hdl.handle.net/11420/3080In 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.enInformatikTechnikMedizinConference Paper10.1007/978-3-030-23703-5_9Other