Open Systems Laboratory at Illinois

Rule-based runtime verification

By Howard Barringer, Allen Goldberg, Klaus Havelund, and Koushik Sen. In VMCAI, volume 2937 of Lecture Notes in Computer Science, 44–57. Springer, 2004.

Full Text:
Download PDF
Publisher Link:


We present a rule-based framework for defining and implementing finite trace monitoring logics, including future and past time temporal logic, extended regular expressions, real-time logics, interval logics, forms of quantified temporal logics, and so on. Our logic, Eagle, is implemented as a Java library and involves novel techniques for rule definition, manipulation and execution. Monitoring is done on a state-by-state basis, without storing the execution trace.


    author = "Barringer, Howard and Goldberg, Allen and Havelund,
              Klaus and Sen, Koushik",
    editor = "Steffen, Bernhard and Levi, Giorgio",
    title = "Rule-Based Runtime Verification",
    booktitle = "VMCAI",
    crossref = "conf/vmcai/2004",
    ee = "",
    keywords = "formal methods, software engineering",
    pages = "44-57",
    year = "2004",

    editor = "Steffen, Bernhard and Levi, Giorgio",
    title = "Verification, Model Checking, and Abstract
             Interpretation, 5th International Conference, VMCAI 2004, Venice,
             January 11-13, 2004, Proceedings",
    isbn = "3-540-20803-8",
    publisher = "Springer",
    series = "Lecture Notes in Computer Science",
    volume = "2937",
    year = "2004",