TY - GEN
T1 - Monitoring programs using rewriting
AU - Havelund, Klaus
AU - Roşu, Grigore
N1 - Publisher Copyright:
© 2001 IEEE.
PY - 2001
Y1 - 2001
N2 - 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 (J P A X) project, the purpose of which is to develop a flexible tool for monitoring Java program executions.
AB - 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 (J P A X) project, the purpose of which is to develop a flexible tool for monitoring Java program executions.
UR - http://www.scopus.com/inward/record.url?scp=85116922800&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85116922800&partnerID=8YFLogxK
U2 - 10.1109/ASE.2001.989799
DO - 10.1109/ASE.2001.989799
M3 - Conference contribution
AN - SCOPUS:85116922800
T3 - Proceedings - 16th Annual International Conference on Automated Software Engineering, ASE 2001
SP - 135
EP - 143
BT - Proceedings - 16th Annual International Conference on Automated Software Engineering, ASE 2001
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 16th Annual IEEE International Conference on Automated Software Engineering, ASE 2001
Y2 - 26 November 2001 through 29 November 2001
ER -