MOPBox: A library approach to runtime verification

Abstract. In this work we propose MOPBox, a library-based approach to runtime verification. MOPBox is a Java library for defining and eval-uating parametric runtime monitors. A user can define monitors through a simple set of API calls. Once a monitor is defined, it is ready to accept events. Events can originate from AspectJ aspects or from other sources, and they can be parametric, i.e., can contain variable bindings that bind abstract specification variables to concrete program values. When a mon-itor reaches an error state for a binding ~v = ~o, MOPBox notifies clients of a match for ~v = ~o through a call-back interface. To map variable bind-ings to monitors, MOPBox uses re-implementations of efficient indexing algorithms that Chen et al. developed for JavaMOP. We took care to keep MOPBox as generic as possible. States, transi-tions and variable bindings can be labeled not just with strings but with general Java Objects whose types are checked through Java Generics. This allows for simple integration into existing tools. For instance, w