LOLA: Runtime Monitoring of Synchronous Systems

TLDR

Monitoring synchronous systems is valuable for both testing and deployment, and a simple, expressive specification language that supports correctness assertions and statistical profiling is essential, especially when memory usage must be bounded for large input streams. The paper introduces a specification language and algorithms for online and offline monitoring of synchronous systems such as circuits and embedded systems. The authors propose a partial‑evaluation based online monitoring algorithm that incrementally builds output streams while keeping memory independent of input length for a syntactically defined class of specifications, and they extend this approach to an efficient offline algorithm for large traces. Implementation on a PCI bus protocol and a memory controller demonstrates that the algorithms are practical and the specification language is expressive enough for industrial use.

Abstract

We present a specification language and algorithms for the online and offline monitoring of synchronous systems including circuits and embedded systems. Such monitoring is useful not only for testing, but also under actual deployment. The specification language is simple and expressive; it can describe both correctness/failure assertions along with interesting statistical measures that are useful for system profiling and coverage analysis. The algorithm for online monitoring of queries in this language follows a partial evaluation strategy: it incrementally constructs output streams from input streams, while maintaining a store of partially evaluated expressions for forward references. We identify a class of specifications, characterized syntactically, for which the algorithm's memory requirement is independent of the length of the input streams. Being able to bound memory requirements is especially important in online monitoring of large input streams. We extend the concepts used in the online algorithm to construct an efficient offline monitoring algorithm for large traces. We have implemented our algorithm and applied it to two industrial systems, the PCI bus protocol and a memory controller. The results demonstrate that our algorithms are practical and that our specification language is sufficiently expressive to handle specifications of interest to industry.