Performance Evaluation of Sensor Networks by Statistical Modeling and Euclidean Model Checking: PhD Oral Exam - Saber Mizraei

Starts:
1:00 pm on Wednesday, December 11, 2013
Ends:
2:00 pm on Wednesday, December 11, 2013
Location:
MCS 137
Authors: Y. Kwon, Microsoft Corporation G. Agha, University of Illinois at Urbana Champaign Presented by: Saber Mirzaei Abstract. Modeling and evaluating the performance of large-scale wireless sensor networks (WSNs) is a challenging problem. One method for formally proving the properties of a system is model checking. However, because of the large number of nodes in a typical WSN, it is difficult to use the traditional representation of global states for model checking. The approach presented in this paper, for addressing the state space explosion problem, is to abstract the global system's state as a probability mass function (pmf), where the pmf represents the fraction of the nodes in certain states. While a pmf abstraction abstracts the state of individual nodes, it provides sufficient information to evaluate the overall performance of a system. Using a pmf representation, one can evaluate the expected behavior of a system for properties such as expected energy consumption, reliability, availability, etc. Moreover, the states (pmf) transition dynamics is modeled as a discrete-time Markov chain (DTMC). In this work, a model checking approach is proposed that quantitively evaluates all state trajectories. Also for the sake of automation of property checking, a temporal logic called iLTL is presented. Finally, approaches for estimating the model of a WSN as well as statistical checking of “the goodness of fit” of the suggested model are covered in this talk.