A joint project of the Graduate School, Peabody College, and the Jean & Alexander Heard Library

Title page for ETD etd-03262009-140102


Type of Document Dissertation
Author Riley, Derek David
URN etd-03262009-140102
Title Modeling, simulation, and verification of biochemical processes using Stochastic Hybrid Systems
Degree PhD
Department Computer Science
Advisory Committee
Advisor Name Title
Xenofon Koutsoukos Committee Chair
Gabor Karsai Committee Member
Gautam Biswas Committee Member
Janos Sztipanovits Committee Member
Larry Dowdy Committee Member
Keywords
  • Biochemistry -- Data processing
  • Hybrid computer simulation
  • Stochastic models
  • verification
  • biochemical modeling
  • simulation
  • Computational biology
  • Monte Carlo method
Date of Defense 2009-03-24
Availability unrestricted
Abstract
Formal modeling and analysis methods hold great promise to help further discovery and innovation for biochemical systems. Domain experts from physicians to chemical engineers can use computational modeling and analysis tools to clarify and demystify complex systems. However, development of accurate and efficient modeling methodologies and analysis techniques pose challenges for biochemical systems. Simulation of biochemical systems is difficult because of the complex dynamics, exhaustive verification methods are computationally expensive for large systems, and Monte Carlo methods are inaccurate and inefficient when rare events are present.

This dissertation uses Stochastic Hybrid Systems (SHS) for modeling and analysis because they can formally capture the complex dynamics of a large class of biochemical systems. An advanced fixed step simulation technique is developed for SHS that employs improved boundary crossing detection methods using probabilistic sampling. Further, an adaptive time stepping simulation method for SHS is implemented to improve accuracy and efficiency. An exhaustive verification method for SHS based on dynamic programming is developed as a tool for analyzing reachability properties for the entire state space. A parallelization of the verification method is developed to improve efficiency. Reachability analysis can also be performed using Monte Carlo methods, so Monte Carlo methods for SHS are implemented. A variance reduction method called MultiLevel Splitting (MLS) is developed for SHS that improves accuracy and efficiency in the presence of rare events. Parameter selection methods are created to help determine appropriate MLS configuration parameters.

Realistic case studies are used to demonstrate the modeling capabilities of SHS and the proposed analysis methods. The case studies include models of sugar cataract development in the lens of a human eye, a commercial biodiesel production system, glycolysis, which is a cellular energy conversion mechanism found in every living cell, and the water and electrolyte balance system in humans. These case studies are used to present experimental results for the analysis methods developed in this work.

Files
  Filename       Size       Approximate Download Time (Hours:Minutes:Seconds) 
 
 28.8 Modem   56K Modem   ISDN (64 Kb)   ISDN (128 Kb)   Higher-speed Access 
  RileyDissertation.pdf 2.82 Mb 00:13:04 00:06:43 00:05:52 00:02:56 00:00:15

Browse All Available ETDs by ( Author | Department )

If you have more questions or technical problems, please Contact LITS.