Formal Network Testing

Certain types of errors, such as hardware failure, link failure or congestion can only be detected at runtime of network as these are failures that happen when the network is in operation. Today, there exist only preliminary tools to detect and pinpoint such kind of errors, typified by ping and trace rout. In this paper we introduce a formal and comprehensive way to fully test networks at runtime which enables us to pinpoint the exact rule that is causing the problem. Our test packet generation algorithm first picks a relatively small number of test packets and corresponding input ports so that these packets exercise all the rules in network. By periodically sending these packets through the network, we can constantly monitor the health of the network. Whenever an error happens, the fault localization algorithm uses the result of all test packets to find out the exact rule that is in fault.