On the construction of monitors for temporal logic properties

M.C.W. Geilen

doi:10.1016/S1571-0661(04)00252-X

On the construction of monitors for temporal logic properties

M.C.W. Geilen

CompSOC Lab- Predictable & Composable Embedded Systems

Research output: Contribution to journal › Article › Academic › peer-review

59 Citations (Scopus)

82 Downloads (Pure)

Abstract

Temporal logic is a valuable tool for specifying correctness properties of reactive programs. With the advent of temporal logic model checkers, it has become an important aid for the verification of concurrent and reactive systems. In model checking the temporal logic properties are verified against models expressed in the tool's modelling language. In addition, model-checking techniques are useful to test actual implementations or to verify models of the system that are too detailed to be analysed by a model checker, by means of, for instance, simulation.

Original language	English
Pages (from-to)	181-199
Journal	Electronic Notes in Theoretical Computer Science
Volume	55
Issue number	2
DOIs	https://doi.org/10.1016/S1571-0661(04)00252-X
Publication status	Published - 2001
Event	RV'01-First Workshop on Runtime Verification - Paris, France Duration: 23 Jul 2001 → 23 Jul 2001

Bibliographical note

Part of special issue:
RV'2001, Runtime Verification (in connection with CAV '01)
Edited by Klaus Havelund, Grigore Rosu

Access to Document

10.1016/S1571-0661(04)00252-X

Publishers versionFinal published version, 352 KB

Cite this

@article{3648585a492044398a34858f5c5eadf4,

title = "On the construction of monitors for temporal logic properties",

abstract = "Temporal logic is a valuable tool for specifying correctness properties of reactive programs. With the advent of temporal logic model checkers, it has become an important aid for the verification of concurrent and reactive systems. In model checking the temporal logic properties are verified against models expressed in the tool's modelling language. In addition, model-checking techniques are useful to test actual implementations or to verify models of the system that are too detailed to be analysed by a model checker, by means of, for instance, simulation.",

author = "M.C.W. Geilen",

note = "Part of special issue: RV'2001, Runtime Verification (in connection with CAV '01) Edited by Klaus Havelund, Grigore Rosu; RV'01-First Workshop on Runtime Verification ; Conference date: 23-07-2001 Through 23-07-2001",

year = "2001",

doi = "10.1016/S1571-0661(04)00252-X",

language = "English",

volume = "55",

pages = "181--199",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

number = "2",

}

TY - JOUR

T1 - On the construction of monitors for temporal logic properties

AU - Geilen, M.C.W.

N1 - Part of special issue: RV'2001, Runtime Verification (in connection with CAV '01) Edited by Klaus Havelund, Grigore Rosu

PY - 2001

Y1 - 2001

N2 - Temporal logic is a valuable tool for specifying correctness properties of reactive programs. With the advent of temporal logic model checkers, it has become an important aid for the verification of concurrent and reactive systems. In model checking the temporal logic properties are verified against models expressed in the tool's modelling language. In addition, model-checking techniques are useful to test actual implementations or to verify models of the system that are too detailed to be analysed by a model checker, by means of, for instance, simulation.

AB - Temporal logic is a valuable tool for specifying correctness properties of reactive programs. With the advent of temporal logic model checkers, it has become an important aid for the verification of concurrent and reactive systems. In model checking the temporal logic properties are verified against models expressed in the tool's modelling language. In addition, model-checking techniques are useful to test actual implementations or to verify models of the system that are too detailed to be analysed by a model checker, by means of, for instance, simulation.

U2 - 10.1016/S1571-0661(04)00252-X

DO - 10.1016/S1571-0661(04)00252-X

M3 - Article

SN - 1571-0661

VL - 55

SP - 181

EP - 199

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 2

T2 - RV'01-First Workshop on Runtime Verification

Y2 - 23 July 2001 through 23 July 2001

ER -

On the construction of monitors for temporal logic properties

Abstract

Bibliographical note

Access to Document

Fingerprint

Cite this