From Specification to Implementation: Assume-Guarantee Contracts for Synthetic Biology

Abstract

We provide a new perspective on using formal methods to model specifications and synthesize implementations for the design of biological circuits. In synthetic biology, design objectives are rarely described formally. We present an assume-guarantee contract framework to describe biological circuit design objectives as formal specifications. In our approach, these formal specifications are implemented by circuits modeled by ordinary differential equations, yielding a design framework that can be used to design complex synthetic biological circuits at scale. We describe our approach using the design of a biological AND gate as a motivating, running example.