@MASTERSTHESIS\{IMM2012-06368,
    author       = "N. Wu",
    title        = "Modelling and Analysis of Wireless Sensor Networks with Energy Harvesting Capabilities",
    year         = "2012",
    school       = "Technical University of Denmark, {DTU} Informatics, {E-}mail: reception@imm.dtu.dk",
    address      = "Asmussens Alle, Building 305, {DK-}2800 Kgs. Lyngby, Denmark",
    type         = "",
    note         = "Supervised by Associate Professor Michael Reichhardt Hansen, mrh@imm.dtu.dk, {DTU} Informatics",
    url          = "http://www.imm.dtu.dk/English.aspx",
    abstract     = "A Wireless Sensor Network is a distributed network, where a large number of autonomous sensor nodes are deployed spatially distributed to monitor physical or environmental conditions, and to cooperatively pass their collected data through the wireless channel to a main location.
In design and development of Wireless Sensor Networks, one of the main challenges is achieving long lasting or even infinite lifetime without human intervention. In order to keep the network alive as long as possible, the best energy-wise route need to be found for each data transfer from a source node to the main location. This is made possible through energy-aware routing. Furthermore, energy harvesting is emerging as a solution for a wide range of Wireless Sensor Networks to provide them to last forever.
Though these technologies are encouraging, there are many potential problems exist. One of which is applying these technologies in sensor nodes cost energy itself. There is a risk that the energy required by using energy-aware routing and energy harvesting may exceed the gain by using them. So, it can be seen as a trade-off in Wireless Sensor Networks between risk and return which need to be tested and analyzed.
This Master’s thesis provides a generic modelling framework which can be used to model and analyze energy harvesting aware Wireless Sensor Networks. Furthermore, a formal model of this framework is developed in {UPPAAL} and will be presented in detail. Besides, a Statistical Model Checking (SMC) extension of {UPPAAL} is applied in the formal model to solve the problem of state-space explosion, and to make the model and the experiments very natural.
With this model in hand, a thorough and formal explanation of energy harvesting aware Wireless Sensor Networks is given. Concrete experiments in terms of simulation and verification, based on the support of {UPPAAL-SMC,} are also available."
}