{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:40:11Z","timestamp":1750203611227,"version":"3.41.0"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2019,3,13]],"date-time":"2019-03-13T00:00:00Z","timestamp":1552435200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1247051 and 1545028"],"award-info":[{"award-number":["1247051 and 1545028"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2019,4,30]]},"abstract":"<jats:p>\n            Watchdog timers are devices that are commonly used to monitor the health of safety-critical hardware and software systems. Their primary function is to raise an alarm if the monitored systems fail to emit periodic \u201cheartbeats\u201d that signal their well-being. In this article, we design and verify a\n            <jats:italic>molecular watchdog timer<\/jats:italic>\n            for monitoring the health of programmed molecular nanosystems. This raises new challenges, because our molecular watchdog timer and the system that it monitors both operate in the probabilistic environment of chemical kinetics, where many failures are certain to occur and it is especially hard to detect the absence of a signal.\n          <\/jats:p>\n          <jats:p>Our molecular watchdog timer is the result of an incremental design process that uses goal-oriented requirements engineering, simulation, stochastic analysis, and software verification tools. We demonstrate the molecular watchdog\u2019s functionality by having it monitor a molecular oscillator. Both the molecular watchdog timer and the oscillator are implemented as chemical reaction networks, which are the current programming language of choice for many molecular programming applications.<\/jats:p>","DOI":"10.1145\/3295740","type":"journal-article","created":{"date-parts":[[2019,3,14]],"date-time":"2019-03-14T17:11:58Z","timestamp":1552583518000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Runtime Fault Detection in Programmed Molecular Systems"],"prefix":"10.1145","volume":"28","author":[{"given":"Samuel J.","family":"Ellis","sequence":"first","affiliation":[{"name":"Molecular Sciences Software Institute, Blacksburg, VA"}]},{"given":"Titus H.","family":"Klinge","sequence":"additional","affiliation":[{"name":"Carleton College, Des Moines, IA"}]},{"given":"James I.","family":"Lathrop","sequence":"additional","affiliation":[{"name":"Iowa State University, Ames, IA"}]},{"given":"Jack H.","family":"Lutz","sequence":"additional","affiliation":[{"name":"Iowa State University, Ames, IA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5390-7982","authenticated-orcid":false,"given":"Robyn R.","family":"Lutz","sequence":"additional","affiliation":[{"name":"Iowa State University, Ames, IA"}]},{"given":"Andrew S.","family":"Miner","sequence":"additional","affiliation":[{"name":"Iowa State University, Ames, IA"}]},{"given":"Hugh D.","family":"Potter","sequence":"additional","affiliation":[{"name":"Iowa State University, Ames, IA"}]}],"member":"320","published-online":{"date-parts":[[2019,3,13]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Kurtz","author":"Anderson David F.","year":"2011","unstructured":"David F. Anderson and Thomas G . Kurtz . 2011 . Continuous time markov chain models for chemical reaction networks. In Design and Analysis of Biomolecular Circuits, Heinz Koeppl, Gianluca Setti, Mario di Bernardo, and Douglas Densmore (Eds.). Springer , 3--42. David F. Anderson and Thomas G. Kurtz. 2011. Continuous time markov chain models for chemical reaction networks. In Design and Analysis of Biomolecular Circuits, Heinz Koeppl, Gianluca Setti, Mario di Bernardo, and Douglas Densmore (Eds.). Springer, 3--42."},{"key":"e_1_2_2_2_1","volume-title":"Kurtz","author":"Anderson David F.","year":"2015","unstructured":"David F. Anderson and Thomas G . Kurtz . 2015 . Stochastic Analysis of Biochemical Systems, Vol . 1.2. Springer International Publishing . David F. Anderson and Thomas G. Kurtz. 2015. Stochastic Analysis of Biochemical Systems, Vol. 1.2. Springer International Publishing."},{"key":"e_1_2_2_3_1","volume-title":"Lahiri","author":"Athreya Krishna B.","year":"2006","unstructured":"Krishna B. Athreya and Soumendra N . Lahiri . 2006 . Measure Theory and Probability Theory. Springer . Krishna B. Athreya and Soumendra N. Lahiri. 2006. Measure Theory and Probability Theory. Springer."},{"doi-asserted-by":"publisher","key":"e_1_2_2_4_1","DOI":"10.1109\/TDSC.2004.2"},{"doi-asserted-by":"publisher","key":"e_1_2_2_5_1","DOI":"10.1145\/343369.343402"},{"doi-asserted-by":"publisher","key":"e_1_2_2_6_1","DOI":"10.1007\/978-3-319-66799-7_15"},{"volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking (Representation and Mind Series) . The MIT Press . Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking (Representation and Mind Series). The MIT Press.","key":"e_1_2_2_7_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_8_1","DOI":"10.1016\/j.tcs.2010.02.010"},{"doi-asserted-by":"publisher","key":"e_1_2_2_9_1","DOI":"10.1016\/j.entcs.2009.02.002"},{"doi-asserted-by":"publisher","key":"e_1_2_2_10_1","DOI":"10.1007\/s00766-013-0168-5"},{"doi-asserted-by":"publisher","key":"e_1_2_2_11_1","DOI":"10.1109\/RE.2014.6912246"},{"volume-title":"Artificial biochemistry","author":"Cardelli Luca","unstructured":"Luca Cardelli . 2009. Artificial biochemistry . In Algorithmic Bioprocesses, Anne Condon, David Harel, Joost N. Kok, Arto Salomaa, and Erik Winfree (Eds.). Springer , Berlin , 429--462. Luca Cardelli. 2009. Artificial biochemistry. In Algorithmic Bioprocesses, Anne Condon, David Harel, Joost N. Kok, Arto Salomaa, and Erik Winfree (Eds.). Springer, Berlin, 429--462.","key":"e_1_2_2_12_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_13_1","DOI":"10.1017\/S0960129512000102"},{"doi-asserted-by":"publisher","key":"e_1_2_2_14_1","DOI":"10.1038\/nnano.2013.189"},{"doi-asserted-by":"publisher","key":"e_1_2_2_15_1","DOI":"10.1007\/978-3-319-11295-4_6"},{"doi-asserted-by":"publisher","key":"e_1_2_2_16_1","DOI":"10.1007\/s10009-014-0323-4"},{"doi-asserted-by":"publisher","key":"e_1_2_2_17_1","DOI":"10.1063\/1.1750549"},{"doi-asserted-by":"publisher","key":"e_1_2_2_18_1","DOI":"10.1126\/science.1214081"},{"key":"e_1_2_2_19_1","first-page":"1","article-title":"Rapid prototyping of 3D DNA-origami shapes with caDNAno","volume":"58","author":"Douglas Shawn M.","year":"2009","unstructured":"Shawn M. Douglas , Adam H. Marblestone , Surat Teerapittayanon , Alejandro Vazquez , George M. Church , and William M. Shih . 2009 . Rapid prototyping of 3D DNA-origami shapes with caDNAno . Nucl. Acids Res. 58 , 24 (2009), 1 -- 6 . Shawn M. Douglas, Adam H. Marblestone, Surat Teerapittayanon, Alejandro Vazquez, George M. Church, and William M. Shih. 2009. Rapid prototyping of 3D DNA-origami shapes with caDNAno. Nucl. Acids Res. 58, 24 (2009), 1--6.","journal-title":"Nucl. Acids Res."},{"volume-title":"Designing a Molecular Watchdog Timer for Safety Critical Systems. Master\u2019s Thesis","author":"Ellis Samuel Jay","unstructured":"Samuel Jay Ellis . 2014. Designing a Molecular Watchdog Timer for Safety Critical Systems. Master\u2019s Thesis . Iowa State University . Samuel Jay Ellis. 2014. Designing a Molecular Watchdog Timer for Safety Critical Systems. Master\u2019s Thesis. Iowa State University.","key":"e_1_2_2_20_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_22_1","DOI":"10.1145\/2642937.2643007"},{"doi-asserted-by":"publisher","key":"e_1_2_2_23_1","DOI":"10.1021\/acssynbio.6b00170"},{"doi-asserted-by":"publisher","key":"e_1_2_2_24_1","DOI":"10.1145\/2001269.2001289"},{"doi-asserted-by":"publisher","key":"e_1_2_2_25_1","DOI":"10.1098\/rsif.2011.0141"},{"volume-title":"Proceedings of the 54th IEEE Conference on Decision and Control (CDC\u201915)","author":"Hori Yutaka","unstructured":"Yutaka Hori and Richard M. Murray . 2015. Engineering principles of synthetic biochemical oscillators with negative cyclic feedback . In Proceedings of the 54th IEEE Conference on Decision and Control (CDC\u201915) . 584--589. Yutaka Hori and Richard M. Murray. 2015. Engineering principles of synthetic biochemical oscillators with negative cyclic feedback. In Proceedings of the 54th IEEE Conference on Decision and Control (CDC\u201915). 584--589.","key":"e_1_2_2_26_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_27_1","DOI":"10.1145\/2024724.2024911"},{"doi-asserted-by":"publisher","key":"e_1_2_2_28_1","DOI":"10.1093\/nar\/gkr1173"},{"volume-title":"Fundamentals of Dependable Computing for Software Engineers","author":"Knight John","unstructured":"John Knight . 2012. Fundamentals of Dependable Computing for Software Engineers . CRC Press . John Knight. 2012. Fundamentals of Dependable Computing for Software Engineers. CRC Press.","key":"e_1_2_2_29_1"},{"key":"e_1_2_2_30_1","volume-title":"Retrieved on","author":"Koopman Phil","year":"2014","unstructured":"Phil Koopman . 2014 . A Case Study of Toyota Unintended Acceleration and Software Safety . Retrieved on February 23, 2019 from https:\/\/users.ece.cmu.edu\/&sim;koopman\/pubs\/koopman14_toyota_ua_slides.pdf. Phil Koopman. 2014. A Case Study of Toyota Unintended Acceleration and Software Safety. Retrieved on February 23, 2019 from https:\/\/users.ece.cmu.edu\/&sim;koopman\/pubs\/koopman14_toyota_ua_slides.pdf."},{"unstructured":"M. Kwiatkowska. 2014. Challenges in automated verification and synthesis for molecular programming. In Essays for the Luca Cardelli Fest. Microsoft Research 155--170.  M. Kwiatkowska. 2014. Challenges in automated verification and synthesis for molecular programming. In Essays for the Luca Cardelli Fest. Microsoft Research 155--170.","key":"e_1_2_2_31_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_32_1","DOI":"10.5555\/2032305.2032352"},{"key":"e_1_2_2_33_1","first-page":"165","article-title":"Probabilistic model checking for biology","volume":"36","author":"Kwiatkowska Marta","year":"2014","unstructured":"Marta Kwiatkowska and Chris Thachuk . 2014 . Probabilistic model checking for biology . Softw. Syst. Saf. 36 (2014), 165 -- 189 . Marta Kwiatkowska and Chris Thachuk. 2014. Probabilistic model checking for biology. Softw. Syst. Saf. 36 (2014), 165--189.","journal-title":"Softw. Syst. Saf."},{"volume-title":"The Computationally Complete Ant Colony: Global Coordination in a System with No Hierarchy","author":"Lachmann Michael","unstructured":"Michael Lachmann and Guy Sella . 1995. The Computationally Complete Ant Colony: Global Coordination in a System with No Hierarchy . Springer , Berlin , 784--800. Michael Lachmann and Guy Sella. 1995. The Computationally Complete Ant Colony: Global Coordination in a System with No Hierarchy. Springer, Berlin, 784--800.","key":"e_1_2_2_34_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_35_1","DOI":"10.1098\/rsif.2011.0343"},{"doi-asserted-by":"publisher","key":"e_1_2_2_36_1","DOI":"10.1093\/bioinformatics\/btr543"},{"doi-asserted-by":"publisher","key":"e_1_2_2_37_1","DOI":"10.1145\/1029894.1029905"},{"doi-asserted-by":"publisher","key":"e_1_2_2_38_1","DOI":"10.1145\/202709"},{"doi-asserted-by":"publisher","key":"e_1_2_2_39_1","DOI":"10.1002\/ijch.201300002"},{"doi-asserted-by":"publisher","key":"e_1_2_2_40_1","DOI":"10.5555\/2337223.2337418"},{"doi-asserted-by":"publisher","key":"e_1_2_2_41_1","DOI":"10.1109\/RE.2012.6345806"},{"doi-asserted-by":"publisher","key":"e_1_2_2_42_1","DOI":"10.1007\/s10270-012-0277-5"},{"doi-asserted-by":"publisher","key":"e_1_2_2_43_1","DOI":"10.1016\/j.ic.2005.05.010"},{"key":"e_1_2_2_44_1","volume-title":"Retrieved on","author":"NASA.","year":"1988","unstructured":"NASA. 1988 . Computers in Spaceflight: The NASA Experience . Retrieved on February 23, 2019 from https:\/\/history.nasa.gov\/computers\/contents.html. NASA. 1988. Computers in Spaceflight: The NASA Experience. Retrieved on February 23, 2019 from https:\/\/history.nasa.gov\/computers\/contents.html."},{"key":"e_1_2_2_45_1","volume-title":"Concrete Semantics","author":"Nipkow Tobias","unstructured":"Tobias Nipkow and Gerwin Klein . 2014. Concrete Semantics ( 1 st ed.). Springer International Publishing . Tobias Nipkow and Gerwin Klein. 2014. Concrete Semantics (1st ed.). Springer International Publishing.","edition":"1"},{"volume-title":"Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle\/HOL","unstructured":"Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle\/HOL ( 1 st ed.). Lecture Notes in Computer Science, Vol. 2283 . Springer-Verlag . Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle\/HOL (1st ed.). Lecture Notes in Computer Science, Vol. 2283. Springer-Verlag.","edition":"1","key":"e_1_2_2_46_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_47_1","DOI":"10.1109\/2.910904"},{"key":"e_1_2_2_48_1","volume-title":"Paulson and Kong Woei Susanto","author":"Lawrence","year":"2007","unstructured":"Lawrence C. Paulson and Kong Woei Susanto . 2007 . Source-level proof reconstruction for interactive theorem proving. In Theorem Proving in Higher Order Logics, Klaus Schneider and Jens Brandt (Eds.). Springer , Berlin, 232--245. Lawrence C. Paulson and Kong Woei Susanto. 2007. Source-level proof reconstruction for interactive theorem proving. In Theorem Proving in Higher Order Logics, Klaus Schneider and Jens Brandt (Eds.). Springer, Berlin, 232--245."},{"doi-asserted-by":"publisher","key":"e_1_2_2_49_1","DOI":"10.1145\/2890494"},{"doi-asserted-by":"publisher","key":"e_1_2_2_50_1","DOI":"10.1098\/rsif.2009.0072.focus"},{"doi-asserted-by":"publisher","key":"e_1_2_2_51_1","DOI":"10.1126\/science.1200520"},{"unstructured":"David Soloveichik. 2008. Molecules Computing: Self-assembled Nanostructures Molecular Automata and Chemical Reaction Networks. Ph.D. Dissertation. California Institute of Technology.   David Soloveichik. 2008. Molecules Computing: Self-assembled Nanostructures Molecular Automata and Chemical Reaction Networks. Ph.D. Dissertation. California Institute of Technology.","key":"e_1_2_2_52_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_53_1","DOI":"10.1007\/s11047-008-9067-y"},{"doi-asserted-by":"publisher","key":"e_1_2_2_54_1","DOI":"10.1073\/pnas.0909380107"},{"key":"e_1_2_2_55_1","volume-title":"Enzyme-free nucleic acid dynamical systems. Science 358, 6369","author":"Srinivas Niranjan","year":"2017","unstructured":"Niranjan Srinivas , James Parkin , Georg Seelig , Erik Winfree , and David Soloveichik . 2017. Enzyme-free nucleic acid dynamical systems. Science 358, 6369 ( 2017 ). Niranjan Srinivas, James Parkin, Georg Seelig, Erik Winfree, and David Soloveichik. 2017. Enzyme-free nucleic acid dynamical systems. Science 358, 6369 (2017)."},{"doi-asserted-by":"publisher","key":"e_1_2_2_56_1","DOI":"10.1109\/ICSE.2017.51"},{"key":"e_1_2_2_57_1","volume-title":"Rosenblum","author":"Su Guoxin","year":"2013","unstructured":"Guoxin Su and David S . Rosenblum . 2013 . Asymptotic bounds for quantitative verification of perturbed probabilistic systems. In Formal Methods and Software Engineering. Lecture Notes in Computer Science, Vol. 8144 . Springer , 297--312. Guoxin Su and David S. Rosenblum. 2013. Asymptotic bounds for quantitative verification of perturbed probabilistic systems. In Formal Methods and Software Engineering. Lecture Notes in Computer Science, Vol. 8144. Springer, 297--312."},{"doi-asserted-by":"publisher","key":"e_1_2_2_58_1","DOI":"10.1098\/rsif.2011.0783"},{"volume-title":"Proceedings of Workshop on Complex Faults and Failures in Large Software Systems.","author":"Tun T.","unstructured":"T. Tun , R. Lutz , B. Nakayama , Y. Yu , D. Mathur , and B. Nuseibeh . 2015. The role of environmental assumptions in failures of DNA nanosystems . In Proceedings of Workshop on Complex Faults and Failures in Large Software Systems. T. Tun, R. Lutz, B. Nakayama, Y. Yu, D. Mathur, and B. Nuseibeh. 2015. The role of environmental assumptions in failures of DNA nanosystems. In Proceedings of Workshop on Complex Faults and Failures in Large Software Systems.","key":"e_1_2_2_59_1"},{"volume-title":"Requirements Engineering\u2014From System Goals to UML Models to Software Specifications","author":"van Lamsweerde Axel","unstructured":"Axel van Lamsweerde . 2009. Requirements Engineering\u2014From System Goals to UML Models to Software Specifications . Wiley . Axel van Lamsweerde. 2009. Requirements Engineering\u2014From System Goals to UML Models to Software Specifications. Wiley.","key":"e_1_2_2_60_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_61_1","DOI":"10.1109\/32.879820"},{"doi-asserted-by":"publisher","key":"e_1_2_2_62_1","DOI":"10.1109\/MS.2012.173"},{"key":"e_1_2_2_63_1","volume-title":"Lin","author":"Wooley John C.","year":"2005","unstructured":"John C. Wooley and Herbert S . Lin . 2005 . Catalyzing Inquiry at the Interface of Computing and Biology. National Academies Press . John C. Wooley and Herbert S. Lin. 2005. Catalyzing Inquiry at the Interface of Computing and Biology. National Academies Press."},{"doi-asserted-by":"publisher","key":"e_1_2_2_64_1","DOI":"10.1007\/978-3-642-38088-4_6"},{"doi-asserted-by":"publisher","key":"e_1_2_2_65_1","DOI":"10.1038\/nchem.957"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3295740","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3295740","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3295740","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:12:50Z","timestamp":1750201970000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3295740"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,3,13]]},"references-count":64,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,4,30]]}},"alternative-id":["10.1145\/3295740"],"URL":"https:\/\/doi.org\/10.1145\/3295740","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2019,3,13]]},"assertion":[{"value":"2017-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-03-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}