Title
Checking Metric Temporal Logic with TRACE
Abstract
Execution traces, time-stamped sequences of events, provide a general, domain-independent, view on the behavior of systems. They enable analysis of metrics such as latency, pipeline depth and throughput. Often, however, it is not clear what such metrics exactly mean and ad hoc methods are used to compute them. Metric Temporal Logic (MTL) can be used to address this issue: it enables the formal specification of quantitative properties on execution traces. We thus have added an MTL checking capability to the TRACE tool, which is a tool for viewing and analyzing execution traces [1]. We use a recursive memoization algorithm that generates concise explanations of the truth value of the given MTL formula. These explanations can be visualized in the TRACE viewer to aid interpretation by the user.
Year
DOI
Venue
2016
10.1109/ACSD.2016.13
2016 16th International Conference on Application of Concurrency to System Design (ACSD)
Keywords
Field
DocType
Metric temporal logic,execution trace,informative prefix,explanation,visualization
Visualization,Latency (engineering),Computer science,Truth value,Theoretical computer science,Formal specification,Real-time computing,Temporal logic,Throughput,Memoization,Recursion
Conference
ISSN
ISBN
Citations 
1550-4808
978-1-5090-0763-9
1
PageRank 
References 
Authors
0.43
7
6
Name
Order
Citations
PageRank
Martijn Hendriks125518.36
Marc Geilen2134684.30
Amir R. B. Behrouzian322.48
Twan Basten41833132.45
Hadi Alizadeh Ara533.50
Dip Goswami627831.58