LOLA: Runtime Monitoring of Synchronous Systems

Abstract

We present a specification language and algorithm for 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, but expressive; it can describe both correctness/failure assertions and 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 inputs, or when input streams are not bounded in advance. We show that the same concepts used in the online algorithm can be used to construct an efficient off-line 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 algorithm is practical and that our specification language is sufficiently expressive to handle specifications of interest to industry.