Fault localization is essential to software maintenance tasks such as testing and automated program repair. Many fault localization techniques have been developed, the most common of which are spectrum-based. Most techniques have been designed for traditional programming paradigms that map passing and failing test cases to lines or branches of code, hence specialized programming paradigms which utilize different code abstractions may fail to localize well. In this paper, we study fault localization in the context of a class of programs, molecular programs. Recent research has designed automated testing and repair frameworks for these pro- grams but has ignored the importance of fault localization. As we demonstrate, using existing spectrum-based approaches may not provide much information. Instead we propose a novel approach, Traceback, that leverages temporal trace data. In an empirical study on a set of 89 faulty program variants, we demonstrate that Trace- back provides between a 32-90% improvement in localization over reaction-based mapping, a direct translation of spectrum-based localization. We see little difference in parameter tuning of Trace- back when all tests, or only code-based (invariant) tests are used, however the best depth and weight parameters vary when using specification based tests, which can be either functional or meta- morphic. Overall, invariant-based tests provide the best localization results (either alone or in combination with others), followed by metamorphic and then functional tests.

Chemical reaction networks (CRNs) are an emerging distributed computational paradigm where programs are encoded as a set of abstract chemical reactions. CRNs can be compiled into DNA strands which perform the computations in vitro, creating a foundation for intelligent nanodevices. Recent research proposed a software testing framework for stochastic CRN programs in simulation, however, it relies on existing program specifications. In practice, specifications are often lacking and when they do exist, transforming them into test cases is time-intensive and can be error prone. In this work, we propose an inference technique called ChemFlow which extracts 3 types of invariants from an existing CRN model. The extracted invariants can then be used for test generation or model validation against program implementations. We applied ChemFlow to 13 CRN programs ranging from toy examples to real biological models with hundreds of reactions. We find that the invariants provide strong fault detection and often exhibit less flakiness than specification derived tests. In the biological models we showed invariants to developers and they confirmed that some of these point to parts of the model that are biologically incorrect or incomplete suggesting we may be able to use ChemFlow to improve model quality.

SafeWalk is a tool kit designed for simulation of a safety-critical product line of astronaut jetpacks. It provides (1) a Unity-based simulation development environment and (2) software artifacts inspired by a real jetpack used by astronauts during spacewalks. SafeWalk has been developed to be a readily extensible and real-time configurable product line for use in research and education. It provides a rich environment conducive to empirical research into safety-critical requirements and to visualization of safety-related human-cyberphysical interactions.

Chemical reaction networks (CRNs) are an important tool for molecular programming, a field that is rapidly expanding our ability to deploy computer programs into biological systems for a variety of applications. However, CRNs are also difficult to work with due to their massively parallel nature, leading to the need for higher-level languages that allow for easier computation with CRNs. Recently, research has been conducted into a variety of higher-level languages for deterministic CRNs but modeling CRN parallelism, managing error accumulation, and finding natural CRN representations are ongoing challenges. We introduce Reactamole, a higher-level language for deterministic CRNs that utilizes the functional reactive programming (FRP) paradigm to represent CRNs as a reactive dataflow network. Reactamole equates a CRN with a functional reactive program, implementing the key primitives of the FRP paradigm directly as CRNs. The functional nature of Reactamole makes reasoning about molecular programs easier, and its strong static typing allows us to ensure that a CRN is well-formed by virtue of being well-typed. In this paper, we describe the design of Reactamole and how we use CRNs to represent the common datatypes and operations found in FRP. We also demonstrate the potential of this functional reactive approach to molecular programming by giving an extended example where a CRN is constructed using FRP to modulate and demodulate an amplitude modulated signal.

In 2015 Schiefer and Winfree introduced the chemical reaction network-controlled tile assembly model (CRN-TAM), a variant of the abstract tile assembly model (aTAM), where tile reactions are mediated via non-local chemical signals. In this paper, we introduce ALCH, an imperative programming language for specifying CRN-TAM programs. ALCH contains common features like Boolean variables, conditionals, and loops. It also supports CRN-TAM-specific features such as adding and removing tiles. A unique feature of the language is the branch statement, a nondeterministic control structure that allows us to query the current state of tile assemblies. We also developed a compiler that translates ALCH to the CRN-TAM, and a simulator that simulates and visualizes the self-assembly of a CRN-TAM program. Using this language, we show that the discrete Sierpinski triangle can be strictly self-assembled in the CRN-TAM. This solves an open problem that the CRN-TAM is capable of self-assembling infinite shapes at scale one that the aTAM cannot. ALCH allows us to present this construction at a high level, abstracting species and reactions into C-like code that is simpler to understand. Our construction utilizes two new CRN-TAM techniques that allow us to tackle this open problem. First, it employs the branching feature of ALCH to probe the previously placed tiles of the assembly and detect the presence and absence of tiles. Second, it uses scaffolding tiles to precisely control tile placement by occluding any undesired binding sites.

We show that very simple molecular systems, modeled as chemical reaction networks, can have behaviors that exhibit dramatic phase transitions at certain population thresholds. Moreover, the magnitudes of these thresholds can thwart attempts to use simulation, model checking, or approximation by differential equations to formally verify the behaviors of such systems at realistic populations. We show how formal theorem provers can successfully verify some such systems at populations where other verification methods fail.

In recent years the use of non-traditional computing mechanisms has grown rapidly. One paradigm uses chemical reaction networks (CRNs) to compute via chemical interactions. CRNs are used to prototype molecular devices at the nanoscale such as intelligent drug therapeutics. In practice, these programs are first written and simulated in environments such as MatLab and later compiled into physical molecules such as DNA strands. However, techniques for testing the correctness of CRNs are lacking. Current methods of validating CRNs include model checking and theorem proving, but these are limited in scalability. In this paper we present the first (to the best of our knowledge) testing framework for CRNs, ChemTest. ChemTest evaluates test oracles on individual simulation traces and supports functional, metamorphic, internal and hyper test cases. It also allows for flakiness and programs that are probabilistic. We performed a large case study demonstrating that ChemTest can find seeded faults and scales beyond model checking. Of our tests, 21% are inherently flaky, suggesting that systematic support for this paradigm is needed. On average, functional tests find 66.5% of the faults, while metamorphic tests find 80.4%, showing the benefit of using metamorphic relationships in our test framework. In addition, we show how the time at evaluation impacts fault detection.

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.

We propose an extension of van Lamsweerde's goal-oriented requirements engineering to the domain of programmable DNA nanotechnology. This is a domain in which individual devices (agents) are at most a few dozen nanometers in diameter. These devices are programmed to assemble themselves from molecular components and perform their assigned tasks. The devices carry out their tasks in the probabilistic world of chemical kinetics, so they are individually error-prone. However, the number of devices deployed is roughly on the order of a nanomole (a 6 followed by fourteen 0s), and some goals are achieved when enough of these agents achieve their assigned subgoals. We show that it is useful in this setting to augment the AND/OR goal diagrams to allow goal refinements that are mediated by threshold functions, rather than ANDs or ORs. We illustrate this method by engineering requirements for a system of molecular detectors (DNA origami “pliers” that capture target molecules) invented by Kuzuya, Sakai, Yamazaki, Xu, and Komiyama (2011). We model this system in the Prism probabilistic symbolic model checker, and we use Prism to verify that requirements are satisfied, provided that the ratio of target molecules to detectors is neither too high nor too low. This gives prima facie evidence that software engineering methods can be used to make DNA nanotechnology more productive, predictable and safe.

DNA nanotechnology uses the information processing capabilities of nucleic acids to design self-assembling, programmable structures and devices at the nanoscale. Devices developed to date have been programmed to implement logic circuits and neural networks, capture or release specific molecules, and traverse molecular tracks and mazes. Here we investigate the use of requirements engineering methods to make DNA nanotechnology more productive, predictable, and safe. We use goal-oriented requirements modeling to identify, specify, and analyze a product family of DNA nanodevices, and we use PRISM model checking to verify both common properties across the family and properties that are specific to individual products. Challenges to doing requirements engineering in this domain include the error-prone nature of nanodevices carrying out their tasks in the probabilistic world of chemical kinetics, the fact that roughly a nanomole (a 1 followed by 14 0s) of devices are typically deployed at once, and the difficulty of specifying and achieving modularity in a realm where devices have many opportunities to interfere with each other. Nevertheless, our results show that requirements engineering is useful in DNA nanotechnology and that leveraging the similarities among nanodevices in the product family improves the modeling and analysis by supporting reuse.

Evolutionary programming of many systems has been demonstrated in the literature. In This work we use these techniques to program a virtual robot to build a wall out of blocks that impede progress in one direction across a grid of squares. Specifically, two methods for automatic program induction are compared on this task. Virtual blocks are presented one at a time in a fixed location on the grid. The robot must move the currently presented block to enable presentation of the next block as well as using the blocks to build the wall. An evolutionary algorithm operating on strings of actions for the task is used for baseline performance measurement. Evolutionary algorithms operating on GP-Automata and ISAc lists are then applied to the wall building task. In addition to broadening the palette of virtual robotics task, this permits us to compare these two representations for program induction. We study two versions of the wall building problem. The first, in which there are impenetrable walls at the boundary of the virtual world, is much easier than the second method that takes place on a virtual table-top where blocks and the robot may fall off. In addition to the usual randomized initialization, a technique for initializing evolutionary runs with already evolved solutions is presented for the string baseline and both program induction representations.