## 1 Introduction  
The phenomenon whereby data are acquired from several network-connected sensors for the purposes of sense-making and intelligent decision-making in smart systems is drastically accelerating. It is expected that there will be increasing numbers of large-scale deployments of devices that are instrumented with multi-modal sensors in the near future (e.g., in cities, transportation, museums, energy systems, _etc._). These sensor devices generally have small form factors and possess limited processing and storage capabilities. In addition, they are typically powered by limited battery supplies and/or energy-harvesting sources. An essential component for the realization of these wireless sensing devices is the data transport service, _i.e._, the 'routing protocol', to carry data from the sensor devices to the back-end servers via one or more (Internet-enabled) gateways, for further processing and analysis. Due to the energy constraints of the nodes and the limited transmission range, the IEEE 802.15.4 standard [1] for low-rate wireless personal area networks (LR-WPANs) is often used for inter-nodal communications. As the transmission range of such a radio is typically limited (often in the range of tens of meters), nodes that are deployed over large spatial regions are expected to communicate to the gateway(s) via multiple hops. Due to these aspects and the few resources of the sensor nodes, providing efficient and reliable routing protocols is an important and challenging problem. For years now, several routing protocols for wireless sensor networks (WSN) have been standardized and developed [2; 3; 4; 5; 6; 7; 8; 9; 10; 11]. While many efforts have been produced for their development, integration and performance evaluation, the conformance testing of their implementations has been somehow neglected. The conformance testing of routing protocols is crucial, as a data transport service that does not behave in its expected manner can have detrimental impacts on data collection and severely impact the overall quality, as well as the usefulness of the system. Furthermore, in large-scale sensor systems, a single bug fix can be an extremely time-consuming and labor intensive process, especially if the nodes are placed in inaccessible locations across varying spatial locations. However, though the conformance testing of these protocols is crucial to the reliability of the systems, there are paradoxically very few works. Indeed, the major ones are mostly dedicated to their performance analysis, application and security studied through simulation or emulation relying on non-formal models [12; 13; 14; 15; 16; 17]. We propose in this paper a formal syntax and semantics to express the requirements of WSN routing protocols and to passively test them on real execution traces. These syntax and semantics do not need to be inevitably used on top of any protocol standard. We herein model and test common WSN requirements, as well as specific ones designed from a novel non-standardized routing protocol. We show that our approach is helpful from the very first stage of the system development life cycle and is complementary to the normalization phase, as well. There are two main ways for testing the conformance of a protocol, either in an active or passive way. While the active ones require a simulation of the implementation under test (IUT) and an important testing architecture, the passive ones are based on the observation of input and output events of an IUTat run-time. Basically, passive testing techniques are applied whenever the state of an IUT cannot be controlled by means of test sequences, either because access to the interfaces of the system is unavailable or a reset of the IUT is undesired. This is specifically the case with the WSN where the topology is dynamic and the testing interfaces not always available. Moreover, in actively testing WSN protocols, we often deal with no direct access, wide fluctuations in the wireless channel and a high dependence on prevailing environmental characteristics.