Methods and Tools for the Analysis, Verification and Synthesis of Genetic Logic Circuits,

Synthetic biology has emerged as an important discipline in which engineers and biologists are working together to design new and useful biological systems composed of genetic circuits. The purpose of developing genetic circuits is to carry out desired logical functions inside a living cell. This usually requires simulating the mathematical models of these genetic circuits and perceive whether or not the circuit behaves appropriately.

Furthermore, synthetic biology utilizes the concepts from electronic design automation (EDA) of abstraction and automated construction to generate genetic circuits with the aim to reduce the in-vitro (wet-lab) experiments. To address this, several automated tools have been developed to improve the process of genetic design automation (GDA) with different capabilities.

This thesis attempts to contribute to the advancement of GDA tools by introducing capabilities which we believe that no other existing GDA tools support. First, we introduce a user-friendly simulation tool, called D-VASim, which allows user to perform virtual laboratory experimentation by dynamically interacting with the model during runtime.

This dynamic interaction with the model gives user a feeling of being in the lab performing wet-lab experiments virtually. This tool allows users to perform both deterministic and stochastic simulations. Next, this dissertation introduces a methodology to perform timing analyses of genetic logic circuits, which allows user to analyze the threshold value and propagation delays of genetic logic circuits.

In this thesis, it has been demonstrated, through in-silico experimentation, that the threshold value and propagation delay plays a vital role in the correct functioning of genetic circuit. It has also been shown how some circuit parameters effect these two important design characteristics. This thesis also introduces an automated approach to analyze the behavior of genetic logic circuits from the simulation data.

With this capability, the boolean logic of complex genetic circuits can be analyzed and/or verified automatically. It is also shown in this thesis that the proposed approach is effective to determine the variation in the behavior of genetic circuits when the circuit’s parameters are changed. In addition, the thesis also attempts to propose a synthesis and technology mapping tool, called GeneTech, for genetic circuits.

It allows users to construct a genetic circuit by only specifying its behavior in the form of boolean expression. For technology mapping, this tool uses a gates library developed by the collective efforts of the researchers at MIT and Boston universities. It is shown experimentally that the tool is able to provide all feasible solutions, containing different genetic components, to achieve the specified boolean behavior.

Finally, it has been shown how D-VASim can be used along with other tools for useful purposes, like model checking. With respect to this, an experimental workflow is proposed for checking genetic circuits using the statistical model checking (SMC) utility of the Uppaal tool and the timing analysis capability of D-VASim.

We further demonstrated how the reliability of a simulation can be improved by using the real parameter values. In this regard, the relationship between the simulation parameters and real parameters have been derived.