DataMonitor - A formal approach for passively testing a MANET routing protocol

By applying formal description techniques and formal testing approaches, it is possible to validate the conformance of implementations to the requirements of communication protocols. However, and particularly in wireless communications systems, most of the testing work is devoted to the evaluation of their performance in a simulated environment without formal descriptions. The current work expands on our formal approach for black-box testing of network protocols implemented in the tool DataMonitor, and it demonstrates its applications for MANET routing protocols through passive testing on OLSR traces. With such application, we show how our formal approach can help express complex properties from data relations in messages and evaluated them on real traces. The results from our experiments with an OLSR implementation are provided.