Model Checking Techniques for the Performance Analysis of Delay Tolerant Networks with on-off Behavior

Sparse network of fixed or mobile wireless devices, where most of the time there does not exist a complete path from a source to a destination are often referred to as Delay Tolerant Networks. The store-carry-and-forward principle, according to which messages can be stored at mobile nodes moving around the network area before being forwarded to the destination, allows the transmission of messages in such systems. In this paper, we use an analytical framework to study Delay Tolerant Networks, based on asCSL model checking techniques. In particular we focus on the case in which fixed sensors exhibit on-off behavior to overcome battery capacity limitations.