Degree Type


Date of Award


Degree Name

Master of Science


Computer Science

First Advisor

James I. Lathrop

Second Advisor

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.


Copyright Owner

Samuel Jay Ellis



File Format


File Size

104 pages