  Synthetic Biology is an interdisciplinary field that utilizes
well-established engineering principles, ranging from electrical, control and
computer systems, for analyzing the biological systems, such as biological
circuits, enzymes, pathways and controllers. Traditionally, these biological
systems, i.e., the genetic circuits are analyzed using paper-and-pencil proofs
and computer-based simulations techniques. However, these methods cannot
provide accurate results due to their inherent limitations such as human
error-proneness, round-off errors and the unverified algorithms present in the
core of the tools, providing such analyses. In this paper, we propose to use
higher-order-logic theorem proving as a complementary technique for analyzing
these systems and thus overcome the above-mentioned issues. In particular, we
propose a higher-order-logic theorem proving based framework to formally reason
about the genetic circuits used in synthetic biology. The main idea is to,
first, model the continuous dynamics of the genetic circuits using differential
equations. The next step is to obtain the systems' transfer function from their
corresponding block diagram representations. Finally, the transfer function
based analysis of these differential equation based models is performed using
the Laplace transform. To illustrate the practical utilization of our proposed
framework, we formally analyze the genetic circuits of activated and repressed
expressions of protein.
