What Packets May Come: Automata for Network Monitoring

We consider the problem of monitoring an interactive device, such as an implementation of a network protocol, in order to check whether its execution is consistent with its specification. At first glance, it appears that a monitor could simply follow the input-output trace of the device and check it against the specification. However, if the monitor is able to observe inputs and outputs only from a vantage point external to the device - as is typically the case - the problem becomes surprisingly difficult. This is because events may be buffered, and even lost, between the monitor and the device, in which case, even for a correctly running device, the trace observed at the monitor could be inconsistent with the specification. In this paper, we formulate the problem of external monitoring as a language recognition problem.