Automated requirements analysis for a molecular watchdog timer
Abstract
Dynamic systems in DNA nanotechnology are often programmed using a chemical reaction network (CRN) model as an intermediate level of abstraction. In this paper, we design and analyze a CRN model of a watchdog timer, a device commonly used to monitor the health of a safety critical system. Our process uses incremental design practices with goal-oriented requirements engineering, software verification tools, and custom software to help automate the software engineering process. The watchdog timer is comprised of three components: an absence detector, a threshold filter, and a signal amplifier. These components are separately designed and verified, and only then composed to create the molecular watchdog timer. During the requirements-design iterations, simulation, model checking, and analysis are used to verify the system. Using this methodology several incomplete requirements and design flaws were found, and the final verified model helped determine specific parameters for biological experiments.
BibTeX
@inproceedings{Ellis-al:ASE14,
author = {Samuel J. Ellis and
Eric R. Henderson and
Titus H. Klinge and
James I. Lathrop and
Jack H. Lutz and
Robyn R. Lutz and
Divita Mathur and
Andrew S. Miner},
title = {Automated requirements analysis for a molecular watchdog timer},
booktitle = {ASE},
pages = {767--778},
publisher = {{ACM}},
year = {2014},
}