Date of Award
Master of Science
James I. Lathrop
Robyn R. Lutz
The programming of matter (molecular programming) is often realized through DNA strand displacement (DSD). Computations and algorithms using DNA strand displacement are often modeled using chemical reaction networks (CRN) that abstract away DNA specific reactions and terminology. These CRNs can yield complex behavior similar to computer programs. If these molecular programs are further used in vivo to effect cell change or fight disease, the molecular program becomes a safety critical system.
In this paper we propose and analyze a molecular watchdog timer, based on a software component often used to monitor the health of a critical system. Using goal-oriented requirements engineering and a stochastic CRN model (SCRN) we design a watchdog timer using two components, a delay clock and a threshold detector. The models are directed, informed, and verified by use of a probabilistic model checker.
Analyzing requirements and the design uncovered several defects that were addressed in subsequent iterations. During each phase, the system was modeled using formal verification tools and simulations to verify correctness of the model. It was found that this iterative methodology with verification was potent at illuminating requirement and design flaws. In addition, the final verified model helped determine specific parameters and molecules for initial biological experiments.
Samuel Jay Ellis
Ellis, Samuel Jay, "Designing a molecular watchdog timer for safety critical systems" (2014). Graduate Theses and Dissertations. 13848.