A Framework for Translation and Validation of Digital Microfluidic Protocols

Modern bio-chemical protocols are complex in design, and hence there may remain errors which need to be fixed before the protocol is taken up for synthesis. In this paper, we propose a framework for easy specification and efficient verification of a bio-chemical protocol description. We propose a simple and intuitive description template for specifying a bio-chemical reaction that is easy to adopt, and we expect the biologists/chemists to use this to express their protocol descriptions. Once that is done, our framework (a) presents a visualization of the protocol description for easy comprehension, and (b) automatically translates the description to a high-level C program, for analysis. This program, along with a set of properties on the final reaction concentration, is passed on to a verification engine, which checks if the protocol description can indeed generate the desired concentrations on the final outputs. We present experimental results on a few bioassay protocols and show the utility of our framework for verifiable protocol design.