Publisher DOI: 10.1007/978-3-030-23703-5_9
Title: A quantitative metric temporal logic for execution-time constrained verification
Language: English
Authors: Lehmann, Sascha 
Antoni, Sven-Thomas 
Schlaefer, Alexander 
Schupp, Sibylle 
Issue Date: 2019
Source: Lecture Notes in Computer Science (11615 LNCS): 170-189 (2019)
Journal or Series Name: Lecture notes in computer science 
Abstract (english): 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.
URI: http://hdl.handle.net/11420/3080
ISBN: 978-303023702-8
ISSN: 0302-9743
Institute: Softwaresysteme E-16 
Medizintechnische Systeme E-1 
Type: InProceedings (Aufsatz / Paper einer Konferenz etc.)
Appears in Collections:Publications without fulltext

Show full item record

Page view(s)

187
Last Week
15
Last month
3
checked on Oct 22, 2020

Google ScholarTM

Check

Add Files to Item

Note about this record

Export

Items in TORE are protected by copyright, with all rights reserved, unless otherwise indicated.