gms | German Medical Science

Introduction: Biomedical sensor networks (BSN) are networks of sensors that, installed on the patient, monitor vital body functions, and alert medical staff when needed; high Quality of Service (QoS) can thus be critical. Yet, maintaining the required QoS conflicts with the restriction on (battery) resources: allowing sleep periods for the nodes saves energy but impairs QoS.

Today, QoS properties of a network are validated using simulation. Model checking could provide proofs, but is known to suffer from the ”state space explosion problem” and might therefore not be applicable to realistic scenarios. In a pioneering project, Tschirner et al. [1] were able to use model checking for a BSN and verified QoS properties for various network topologies and different temporal settings. Depending on the particular QoS property, the authors could verify up to 16-node networks; they had to make simplifying assumptions, though. We lift two of those simplifications and empirically evaluate the resulting impact on model checking.

Material and Methods: The models target the Chipcon CC2420 transceiver [2], a popular receiver for wireless communication. Model checking is done by the UPPAAL tool suite [3]. The two QoS properties of interest is the sink connectivity, measuring how long a node needs in the worst case to connect to the sink (i.e., the medical center) possibly through multi-hop connections, and the packet delivery ratio, measuring the ratio of the packages sent that were actually received by the sink.

In the reference model, an acknowledgment status for a packet is set to true for all nodes in the network when the sink node receives the packet. Since such an action is not realistic, in our model, the sink instead sends an acknowledgment for each packet back to all connected nodes.

Also, in our extended model, a node retransmits packets after a timeout as many times as possible, while the reference model permits one retransmission only.

Result: We show that nodes that have a key forwarding role for packets of other nodes towards the sink, provably demand less sleep time. On the other hand, sleep time needs to be increased in points of the network where collisions occur.

We used both the reference and our extended model for verifying the same network topologies, and compared the results.

The behavior of the models and the optimal settings for active and sleep time are similar. Despite careful tuning [4], however, our more complex model veri?es only networks up to 3 nodes. The reference model scales better, in particular when collisions occur. Thus, carefully applied simplifications can enhance a model’s scalability.

Discussion: Model checking is a promising technique for BSNs, but small changes in the complexity of the network topology or the behavior of nodes can have big impact on the size of the network that can be verified. The trade-off between realistic assumptions and scalability suggests to model a node not in its entirety, but to model its components separately, at possibly di?erent abstraction levels, and thereby mitigate the state space explosion problem.