Checking metric temporal logic with TRACE

M. Hendriks; M.C.W. Geilen; A.R.B. Behrouzian; A.A. Basten; H. Alizadeh; D. Goswami

doi:10.1109/ACSD.2016.13

Checking metric temporal logic with TRACE

M. Hendriks
, M.C.W. Geilen
, A.R.B. Behrouzian
, A.A. Basten
, H. Alizadeh
, D. Goswami

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

5 Citaten (Scopus)

1 Downloads (Pure)

Samenvatting

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.

Originele taal-2	Engels
Titel	Proceedings - 2016 16th International Conference on Application of Concurrency to System Design, ACSD 2016, 19-21 June 2016, Turan, Poland
Plaats van productie	Piscataway
Uitgeverij	Institute of Electrical and Electronics Engineers
Pagina's	19-24
Aantal pagina's	6
ISBN van elektronische versie	978-1-5090-2589-3
ISBN van geprinte versie	978-1-5090-0763-9
DOI's	https://doi.org/10.1109/ACSD.2016.13
Status	Gepubliceerd - 3 feb. 2017
Evenement	16th International Conference on Application of Concurrency to System Design (ACSD 2016) - Torun, Polen Duur: 19 jun. 2016 → 21 jun. 2016 Congresnummer: 16 http://pn2016.mat.umk.pl/

Congres

Congres	16th International Conference on Application of Concurrency to System Design (ACSD 2016)
Verkorte titel	ACSD 2016
Land/Regio	Polen
Stad	Torun
Periode	19/06/16 → 21/06/16
Internet adres	http://pn2016.mat.umk.pl/

Toegang tot document

10.1109/ACSD.2016.13

Andere bestanden en links

Link to publication in Scopus

Citeer dit

Hendriks, M., Geilen, M. C. W., Behrouzian, A. R. B., Basten, A. A., Alizadeh, H., & Goswami, D. (2017). Checking metric temporal logic with TRACE. In Proceedings - 2016 16th International Conference on Application of Concurrency to System Design, ACSD 2016, 19-21 June 2016, Turan, Poland (blz. 19-24). Artikel 7842497 Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/ACSD.2016.13

@inproceedings{ffa8d51e8ecb4cf9ab3b192226dd0b01,

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.",

keywords = "execution trace, explanation, informative prefix, Metric temporal logic, visualization",

author = "M. Hendriks and M.C.W. Geilen and A.R.B. Behrouzian and A.A. Basten and H. Alizadeh and D. Goswami",

year = "2017",

month = feb,

day = "3",

doi = "10.1109/ACSD.2016.13",

language = "English",

isbn = "978-1-5090-0763-9 ",

pages = "19--24",

booktitle = "Proceedings - 2016 16th International Conference on Application of Concurrency to System Design, ACSD 2016, 19-21 June 2016, Turan, Poland",

publisher = "Institute of Electrical and Electronics Engineers",

address = "United States",

note = "16th International Conference on Application of Concurrency to System Design (ACSD 2016), ACSD 2016 ; Conference date: 19-06-2016 Through 21-06-2016",

url = "http://pn2016.mat.umk.pl/",

}

Hendriks, M, Geilen, MCW, Behrouzian, ARB, Basten, AA, Alizadeh, H & Goswami, D 2017, Checking metric temporal logic with TRACE. in Proceedings - 2016 16th International Conference on Application of Concurrency to System Design, ACSD 2016, 19-21 June 2016, Turan, Poland., 7842497, Institute of Electrical and Electronics Engineers, Piscataway, blz. 19-24, 16th International Conference on Application of Concurrency to System Design (ACSD 2016), Torun, Polen, 19/06/16. https://doi.org/10.1109/ACSD.2016.13

Checking metric temporal logic with TRACE. / Hendriks, M.; Geilen, M.C.W.; Behrouzian, A.R.B. et al.
Proceedings - 2016 16th International Conference on Application of Concurrency to System Design, ACSD 2016, 19-21 June 2016, Turan, Poland. Piscataway: Institute of Electrical and Electronics Engineers, 2017. blz. 19-24 7842497.

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

TY - GEN

T1 - Checking metric temporal logic with TRACE

AU - Hendriks, M.

AU - Geilen, M.C.W.

AU - Behrouzian, A.R.B.

AU - Basten, A.A.

AU - Alizadeh, H.

AU - Goswami, D.

N1 - Conference code: 16

PY - 2017/2/3

Y1 - 2017/2/3

N2 - 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.

AB - 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.

KW - execution trace

KW - explanation

KW - informative prefix

KW - Metric temporal logic

KW - visualization

UR - https://www.scopus.com/pages/publications/85014968068

U2 - 10.1109/ACSD.2016.13

DO - 10.1109/ACSD.2016.13

M3 - Conference contribution

SN - 978-1-5090-0763-9

SP - 19

EP - 24

BT - Proceedings - 2016 16th International Conference on Application of Concurrency to System Design, ACSD 2016, 19-21 June 2016, Turan, Poland

PB - Institute of Electrical and Electronics Engineers

CY - Piscataway

T2 - 16th International Conference on Application of Concurrency to System Design (ACSD 2016)

Y2 - 19 June 2016 through 21 June 2016

ER -

Hendriks M, Geilen MCW, Behrouzian ARB, Basten AA, Alizadeh H, Goswami D. Checking metric temporal logic with TRACE. In Proceedings - 2016 16th International Conference on Application of Concurrency to System Design, ACSD 2016, 19-21 June 2016, Turan, Poland. Piscataway: Institute of Electrical and Electronics Engineers. 2017. blz. 19-24. 7842497 doi: 10.1109/ACSD.2016.13

Checking metric temporal logic with TRACE

Samenvatting

Congres

Toegang tot document

Andere bestanden en links

Vingerafdruk

Citeer dit