Abstract:
Runtime verification is aimed at analyzing execution
traces stemming from a running program or system. The
traditional purpose is to detect the lack of conformance with
respect to a formal specification. Numerous efforts in the field
have focused on monitoring so-called parametric specifications,
where events carry data, and formulas can refer to such. Since
a monitor for such specifications has to store observed data, the
challenge is to have an efficient representation and manipulation
of Boolean operators, quantification, and lookup of data. The
fundamental problem is that the actual values of the data are
not necessarily bounded or provided in advance. In this work
we explore the use of Binary Decision Diagrams (BDDs) for
representing observed data. Our experiments show a substantial
improvement in performance compared to related work.
