conclusion.tex

\section{Conclusions}
\label{sec:conclusion}

We formally define an instance of the uncertainty problem in validating wireless protocol
implementations using sniffers. We describe a systematic augmentation of the
protocol state machine to explicitly encode the uncertainty of sniffer traces.
We characterize the NP-completeness of the problem and propose both an
exhaustive search algorithm and heuristics to restrict the search to more likely
traces. We present two case studies using \ns{} network simulator to demonstrate
how our framework can improve validation precision and detect real bugs. We also
report the application of our framework on a commercial product under
development.

Finally, we discuss a few challenges and future
directions.

\textbf{Verification Coverage.} Given a single sniffer trace, it is possible
that not all the states in the state machine are visited during the verification
process. For instance, a rate control state machine based on certain consecutive
packet losses patterns can not be verified if no such consecutive losses appear
in the sniffer trace. In general, given a protocol state machine, it is
challenging to extract the packet patterns for each state to be reached and to
alter the testing such that such patterns can be observed.

\textbf{Automated State Machine Construction.} We manually constructed the
protocol monitor state machines for the protocols studied in this paper based on
the source code, comments and documentation. The process involves lots of labor
effort and is time-consuming. A potential alternative is to automatically learn
the sketch of the monitor state machines from the sniffer traces. Domain
knowledge can then be leveraged to improve the sketch state machines.