A theory of monitors

Abstract

We develop a behavioural theory for monitors, computational entities that passively analyse the runtime behaviour of systems so as to infer properties about them. First, we present a monitor language and an instrumentation relation used for piCalculus process monitoring. We then identify contextual behavioural preorders that allow us to relate monitors according to criteria defined over monitored executions of piCalculus processes. Subsequently, we develop alternative monitor preorders that are compositional, since they allow us to relate monitors without resorting to their composite behaviour when they instrumented with systems. Importantly, we show that the latter alternative preorders are sound and complete with respect to the contextual preorders. Finally, we demonstrate how these preorders can assist the development of correct monitor synthesis tools.