  The design of genetic networks with specific functions is one of the major
goals of synthetic biology. However, constructing biological devices that work
"as required" remains challenging, while the cost of uncovering flawed designs
experimentally is large. To address this issue, we propose a fully automated
framework that allows the correctness of synthetic gene networks to be formally
verified in silico from rich, high level functional specifications.
  Given a device, we automatically construct a mathematical model from
experimental data characterizing the parts it is composed of. The specific
model structure guarantees that all experimental observations are captured and
allows us to construct finite abstractions through polyhedral operations. The
correctness of the model with respect to temporal logic specifications can then
be verified automatically using methods inspired by model checking.
  Overall, our procedure is conservative but it can filter through a large
number of potential device designs and select few that satisfy the
specification to be implemented and tested further experimentally. Illustrative
examples of the application of our methods to the design of simple synthetic
gene networks are included.
