论文标题
关于数字微流体生物芯片的生化协议实现的自动正确性检查的框架
A Framework for Automated Correctness Checking of Biochemical Protocol Realizations on Digital Microfluidic Biochips
论文作者
论文摘要
数字微流体（DMF）技术的最新进展为多种生化应用提供了一个有希望的平台，例如DNA分析，自动化药物发现和毒性监测。为了实施复杂的生物测定，已经开发了自动合成工具来应对设计挑战。当前，合成工具通过了许多复杂的设计步骤，以实现目标DMF体系结构的给定生化协议。因此，在综合步骤中可能会出现设计错误。在将DMF生物芯片部署在安全关键系统上之前，有必要确保正确实施所需的生化协议，即，合成输出（生物芯片的驱动序列）是否没有任何设计或实现错误。我们提出了一个基于符号约束的分析框架，用于检查有关原始设计规范的合成生化协议的正确性。基于此框架的验证方案可以检测几种基于2D阵列或受PIN限制的生物芯片以及网络物理系统中的几种合成后流体违规和实现错误。它进一步生成诊断反馈以进行错误定位。我们提出了有关聚合酶链反应（PCR）和维特罗多重生物测定的实验结果，以证明所提出的验证方法。
Recent advances in digital microfluidic (DMF) technologies offer a promising platform for a wide variety of biochemical applications, such as DNA analysis, automated drug discovery, and toxicity monitoring. For on-chip implementation of complex bioassays, automated synthesis tools have been developed to meet the design challenges. Currently, the synthesis tools pass through a number of complex design steps to realize a given biochemical protocol on a target DMF architecture. Thus, design errors can arise during the synthesis steps. Before deploying a DMF biochip on a safety critical system, it is necessary to ensure that the desired biochemical protocol has been correctly implemented, i.e., the synthesized output (actuation sequences for the biochip) is free from any design or realization errors. We propose a symbolic constraint-based analysis framework for checking the correctness of a synthesized biochemical protocol with respect to the original design specification. The verification scheme based on this framework can detect several post-synthesis fluidic violations and realization errors in 2D-array based or pin-constrained biochips as well as in cyberphysical systems. It further generates diagnostic feedback for error localization. We present experimental results on the polymerase chain reaction (PCR) and in-vitro multiplexed bioassays to demonstrate the proposed verification approach.
