Probabilistic Modeling and Verification of Large Scale Systems
Kwon, YoungMin
This item is only available for download by members of the University of Illinois community. Students, faculty, and staff at the U of I may log in with your NetID and password to view the item. If you are trying to access an Illinois-restricted dissertation or thesis, you can request a copy through your library's Inter-Library Loan office or purchase a copy directly from ProQuest.
Permalink
https://hdl.handle.net/2142/81718
Description
Title
Probabilistic Modeling and Verification of Large Scale Systems
Author(s)
Kwon, YoungMin
Issue Date
2006
Doctoral Committee Chair(s)
Agha, Gul A.
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Keyword(s)
Computer Science
Language
eng
Abstract
Many large scale systems have a stochastic behavior. Such stochastic behavior is the result of the randomness in the systems' operating environments. It can also be the result of the use of randomized protocols that are used to reduce the need for costly synchronization. We abstract a system state as a probability mass function (pmf); a pmf is succinct in representation and is informative enough to describe many useful aggregate behaviors of the system. We model the dynamics of the state transitions as a Discrete Time Markov Chain (DTMC) and develop an on-line model estimation method as well as a goodness of fit test that statistically validates the model. We develop a probabilistic temporal logic called iLTL in order to specify aggregate behaviors of large scale systems. Many important performance criteria on DTMC models can be accurately expressed in iLTL. For the iLTL specifications, performance evaluation is systematically performed through a process of model checking. If a performance criterion is not satisfiable, the model checker returns a sequence of computations that violates the specification in order to help users fix the problem. We show the usefulness of our methodology through an experiment with a wireless sensor network of 90 nodes.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
