Skip to main content


CaVi — simulation and model checking for wireless sensor networks


Thanassis Boulis, Ansgar Fehnker, Matthias Fruth and Annabelle McIver


University of Oxford

Macquarie University


CaVi provides a uniform interface to state-of-the-art simulation methods and formal verification methods for wireless sensor network. Simulation is suitable to examine the behavior of a wireless sensor network in great detail. Due to the probabilistic behavior of these systems, however, the simulation covers only a small fraction of all possible behaviors. Formal model checking techniques, based on Markov Decision Processes, use less detailed and more abstract models and compute exact probabilities and expected values for the entire behavior, where simulation can only give averages. CaVi allows for creating a single model for simulation, Monte-Carlo simulation, and model checking.

BibTeX Entry

    publisher        = {Springer},
    author           = {Boulis, Thanassis and Fehnker, Ansgar and Fruth, Matthias and McIver, Annabelle},
    month            = sep,
    editor           = {{S. Donatelli and P. Panangaden}},
    year             = {2008},
    keywords         = {wireless sensor networks, simulation, model checking, graphical front-end},
    title            = {{CaVi} --- Simulation and Model Checking for Wireless Sensor Networks},
    booktitle        = {5th International Conference on Quantitative Evaluation of Systems (QEST 2008)},
    address          = {Saint Malo, France}


Served by Apache on Linux on seL4.