Synthesizing monitors for safety properties

Klaus Havelund; Grigore Rosu

doi:10.1007/3-540-46002-0_24

Synthesizing monitors for safety properties

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

The problem of testing a linear temporal logic (LTL) formula on a finite execution trace of events, generated by an executing program, occurs naturally in runtime analysis of software. An algorithm which takes a past time LTL formula and generates an efficient dynamic programming algorithm is presented. The generated algorithm tests whether the formula is satisfied by a finite trace of events given as input and runs in linear time, its constant depending on the size of the LTL formula. The memory needed is constant, also depending on the size of the formula. Further optimizations of the algorithm are suggested. Past time operators suitable for writing succinct specifications are introduced and shown definitionally equivalent to the standard operators. This work is part of the PathExplorer project, the objective of which it is to construct a flexible framework for monitoring and analyzing program executions.

Original language	English (US)
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems - 8th Int. Conf., TACAS 2002, Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2002, Proc.
Editors	Joost-Pieter Katoen, Perdita Stevens
Publisher	Springer
Pages	342-356
Number of pages	15
ISBN (Print)	3540434194, 9783540434191
DOIs	https://doi.org/10.1007/3-540-46002-0_24
State	Published - 2002
Externally published	Yes
Event	8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Proceedings - Grenoble, France Duration: Apr 8 2002 → Apr 12 2002

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2280 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Proceedings
Country/Territory	France
City	Grenoble
Period	4/8/02 → 4/12/02

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Online availability

10.1007/3-540-46002-0_24

Library availability

Discover UIUC Full Text

Cite this

Havelund, K., & Rosu, G. (2002). Synthesizing monitors for safety properties. In J-P. Katoen, & P. Stevens (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 8th Int. Conf., TACAS 2002, Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2002, Proc. (pp. 342-356). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2280 LNCS). Springer. https://doi.org/10.1007/3-540-46002-0_24

Synthesizing monitors for safety properties. / Havelund, Klaus; Rosu, Grigore.
Tools and Algorithms for the Construction and Analysis of Systems - 8th Int. Conf., TACAS 2002, Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2002, Proc.. ed. / Joost-Pieter Katoen; Perdita Stevens. Springer, 2002. p. 342-356 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2280 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Havelund, K & Rosu, G 2002, Synthesizing monitors for safety properties. in J-P Katoen & P Stevens (eds), Tools and Algorithms for the Construction and Analysis of Systems - 8th Int. Conf., TACAS 2002, Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2002, Proc.. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2280 LNCS, Springer, pp. 342-356, 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Proceedings, Grenoble, France, 4/8/02. https://doi.org/10.1007/3-540-46002-0_24

Havelund K, Rosu G. Synthesizing monitors for safety properties. In Katoen J-P, Stevens P, editors, Tools and Algorithms for the Construction and Analysis of Systems - 8th Int. Conf., TACAS 2002, Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2002, Proc.. Springer. 2002. p. 342-356. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-46002-0_24

Havelund, Klaus ; Rosu, Grigore. / Synthesizing monitors for safety properties. Tools and Algorithms for the Construction and Analysis of Systems - 8th Int. Conf., TACAS 2002, Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2002, Proc.. editor / Joost-Pieter Katoen ; Perdita Stevens. Springer, 2002. pp. 342-356 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{04398bb2a02c4033a8cbe1db754fe284,

title = "Synthesizing monitors for safety properties",

abstract = "The problem of testing a linear temporal logic (LTL) formula on a finite execution trace of events, generated by an executing program, occurs naturally in runtime analysis of software. An algorithm which takes a past time LTL formula and generates an efficient dynamic programming algorithm is presented. The generated algorithm tests whether the formula is satisfied by a finite trace of events given as input and runs in linear time, its constant depending on the size of the LTL formula. The memory needed is constant, also depending on the size of the formula. Further optimizations of the algorithm are suggested. Past time operators suitable for writing succinct specifications are introduced and shown definitionally equivalent to the standard operators. This work is part of the PathExplorer project, the objective of which it is to construct a flexible framework for monitoring and analyzing program executions.",

author = "Klaus Havelund and Grigore Rosu",

year = "2002",

doi = "10.1007/3-540-46002-0_24",

language = "English (US)",

isbn = "3540434194",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "342--356",

editor = "Joost-Pieter Katoen and Perdita Stevens",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 8th Int. Conf., TACAS 2002, Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2002, Proc.",

address = "Germany",

note = "8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Proceedings ; Conference date: 08-04-2002 Through 12-04-2002",

}

TY - GEN

T1 - Synthesizing monitors for safety properties

AU - Havelund, Klaus

AU - Rosu, Grigore

PY - 2002

Y1 - 2002

N2 - The problem of testing a linear temporal logic (LTL) formula on a finite execution trace of events, generated by an executing program, occurs naturally in runtime analysis of software. An algorithm which takes a past time LTL formula and generates an efficient dynamic programming algorithm is presented. The generated algorithm tests whether the formula is satisfied by a finite trace of events given as input and runs in linear time, its constant depending on the size of the LTL formula. The memory needed is constant, also depending on the size of the formula. Further optimizations of the algorithm are suggested. Past time operators suitable for writing succinct specifications are introduced and shown definitionally equivalent to the standard operators. This work is part of the PathExplorer project, the objective of which it is to construct a flexible framework for monitoring and analyzing program executions.

AB - The problem of testing a linear temporal logic (LTL) formula on a finite execution trace of events, generated by an executing program, occurs naturally in runtime analysis of software. An algorithm which takes a past time LTL formula and generates an efficient dynamic programming algorithm is presented. The generated algorithm tests whether the formula is satisfied by a finite trace of events given as input and runs in linear time, its constant depending on the size of the LTL formula. The memory needed is constant, also depending on the size of the formula. Further optimizations of the algorithm are suggested. Past time operators suitable for writing succinct specifications are introduced and shown definitionally equivalent to the standard operators. This work is part of the PathExplorer project, the objective of which it is to construct a flexible framework for monitoring and analyzing program executions.

UR - http://www.scopus.com/inward/record.url?scp=84888249425&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84888249425&partnerID=8YFLogxK

U2 - 10.1007/3-540-46002-0_24

DO - 10.1007/3-540-46002-0_24

M3 - Conference contribution

AN - SCOPUS:84888249425

SN - 3540434194

SN - 9783540434191

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 342

EP - 356

BT - Tools and Algorithms for the Construction and Analysis of Systems - 8th Int. Conf., TACAS 2002, Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2002, Proc.

A2 - Katoen, Joost-Pieter

A2 - Stevens, Perdita

PB - Springer

T2 - 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Proceedings

Y2 - 8 April 2002 through 12 April 2002

ER -

Synthesizing monitors for safety properties

Abstract

Publication series

Other

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this