@inproceedings{havelund-rosu-2001-ase,
author = {Klaus Havelund and Grigore Rosu},
title = {Monitoring Programs using Rewriting},
abstract = {
We present a rewriting algorithm for efficiently testing future time
Linear Temporal Logic (LTL) formulae on finite execution traces. The
standard models of LTL are infinite traces, reflecting the behavior of
reactive and concurrent systems which conceptually may be continuously
alive. In most past applications of LTL, theorem provers and model
checkers have been used to formally prove that down-scaled models
satisfy such LTL specifications. Our goal is instead to use LTL for
up-scaled testing of real software applications, corresponding to
analyzing the conformance of finite traces against LTL formulae. We
first describe what it means for a finite trace to satisfy an LTL
formula and then suggest an optimized algorithm based on transforming
LTL formulae. We use the Maude rewriting logic, which turns out to be
a good notation and being supported by an efficient rewriting engine
for performing these experiments. The work constitutes part of the
Java PathExplorer (\JPaXX) project, the purpose of which is to develop
a flexible tool for monitoring Java program executions.
},
booktitle = {Proceedings of 16th IEEE International Conference. Automated Software Engineering (ASE'01)},
pages = {135-143},
month = {May},
year = {2001},
publisher = {IEEE},
presentation = {2001-11-ASE},
doi = {http://dx.doi.org/10.1109/ASE.2001.989799},
author_id = {Klaus Havelund and Grigore Rosu},
category = {runtime_verification, testing, javamop, rewrite_logic},
project_name = {MOP},
project_url = {http://fsl.cs.illinois.edu/MOP},
booktitle_acronym = {ASE'01},
booktitle_url = {http://ase-conferences.org/ase/past/ase2001/},
}