Correctness Checking of Bio-chemical Protocol Realizations on a Digital Microfluidic Biochip

Recent advances in digital micro fluidic (DMF) technologies offer a promising platform for a wide variety of bio-chemical applications, such as DNA analysis, automated drug discovery, and toxicity monitoring. For on-chip implementation of complex bioassays, automated synthesis tools are now being used in order to meet the increasing design challenges. Currently, the synthesis tools cycle through a number of complex design steps to realize a given bio-chemical protocol on a target DMF architecture. Thus, several design errors are likely to creep into the synthesis process. Before deploying a DMF biochip on a safety critical system, it is becoming mandatory to ensure that the desired bio-chemical protocol has been correctly implemented, i.e., the synthesized output (actuation sequences for the biochip) is free from any design or realization errors. In this paper, we propose a symbolic constraint-based analysis and verification framework for checking the correctness of a synthesized bio-chemical protocol with respect to the original design specification. The proposed framework detects realization errors and generates diagnostic feedback to indicate the possible sources of design rule violations. We have developed a tool that implements our strategy and we present some experimental results on the polymerase chain reaction (PCR).