数字微流控生物芯片上生化协议实现的自动正确性检验框架
A Framework for Automated Correctness Checking of Biochemical Protocol Realizations on Digital Microfluidic Biochips
摘要：
数字微流控（DMF）技术的最新进展为各种生化应用提供了一个有前途的平台，如DNA分析，自动药物发现和毒性监测。为了在芯片上实现复杂的生物测定，已经开发了自动化合成工具来满足设计挑战。目前，合成工具通过许多复杂的设计步骤，以实现目标DMF架构上的给定生物化学方案。因此，在合成步骤期间可能出现设计误差。在安全关键系统上部署DMF生物芯片之前，必须确保正确实施了所需的生化方案，即，合成输出（生物芯片的致动序列）没有任何设计或实现误差。我们提出了一个基于符号约束的分析框架，用于检查合成的生化协议相对于原始设计规范的正确性。基于该框架的验证方案可以检测基于二维阵列或引脚约束的生物芯片以及网络物理系统中的几种合成后流体违规和实现错误。它还生成用于错误定位的诊断反馈。我们目前的聚合酶链反应（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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
