Requirements Engineering for Programmable, Self-Assembling Nanomachines

Programmable DNA nanotechnology is a rapidly emerging field that creates and programs a wide variety of synthetic nanosystems to autonomously assemble themselves from molecular components and perform their assigned tasks. Programming is done by carefully choosing the molecular strands and their concentrations such that they will achieve the desired shape, structure, function or dynamic behavior.

We are interested in the requirements for these programmed systems. What does it mean to specify and validate requirements on programmable DNA self-assemblies? How can we verify formally that a self-assembly satisfies its requirements? It is especially important to begin answering these questions now because envisioned future uses will be safety-critical (e.g., RNA nanomachines embedded in human cells).

We propose an extension of van Lamsweerde's goal-oriented requirements engineering to the domain of programmable DNA nanotechnology. We explain this extended method and illustrate it 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 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.