FMitF: Track I: Correct-by-Construction Synthesis of Microfluidic Chips

FMITF：轨道 I：微流控芯片的构建正确合成

• 批准号: 2019362
• 负责人: Manu Sridharan
• 金额: $ 74.91万
• 依托单位: University of California-Riverside
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-10-01 至 2024-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2019362&HistoricalAwards=false
• 关键词: FMitF; Track; Correct; Construction; Synthesis

The burgeoning field of microfluidics and laboratory-on-a-chip technologies enables miniaturization and automation of chemical and life-science experiments, potentially yielding dramatic efficiency improvements for critical fields like drug discovery and biotechnology. However, designing a microfluidic chip and implementing the associated software currently requires a great deal of manual, error-prone work, negating some of the productivity gains from the technology. This project investigates algorithms that automatically synthesize complete and correct microfluidic chip systems. The project’s novelties are that it aims to be the first to simultaneously synthesize a programmable mechanical object (in this case, a microfluidic chip) in conjunction with the software that controls it, including customization of the chip design to meet the constraints imposed by the equipment in a specific researcher’s laboratory. The project’s impacts are that it broadens the usability of microfluidic technologies, catalyzing new microfluidic applications, new interdisciplinary research, and new commercial opportunities for microfluidics.Within the larger context of formal methods and design automation for microfluidic chips, the project aims to produce the first techniques to synthesize correct-by-construction microfluidic components, multi-component microfluidic chips, and control programs for microfluidics. The project investigates a novel counterexample-guided inductive microfluidic synthesis (CEGIMS) algorithm, in which a microfluidic-chip synthesizer and a control program synthesizer are combined to synergistically generate both a microfluidic chip design and the corresponding control software for available equipment. Users provide sketches of both the microfluidic-chip geometry and control-software structure, along with evaluation criteria specifying the user’s expectations for the physical properties of the fluid flowing inside of the chip. CEGIMS integrates physical-modeling software with Satisfiability Modulo Theory (SMT) solvers, relying on counterexample-guided search methods to complete the sketches, yielding a final chip layout suitable for fabrication. At the same time, CEGIMS automatically synthesizes control software that is guaranteed to drive the chip correctly. In order to achieve these technical goals, the project aims to develop fundamental advances in techniques to integrate solvers based on logical correctness properties with simulation software that determines the correctness of a physical model.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

微流控和芯片实验室技术的新兴领域使化学和生命科学实验实现小型化和自动化，可能为药物发现和生物技术等关键领域带来巨大的效率。然而，设计微流控芯片并实现相关软件。目前需要大量容易出错的手动工作，从而抵消了该技术所带来的一些生产力收益。该项目研究自动合成完整且正确的微流控芯片系统的算法。旨在成为第一个同时合成可编程机械物体（在本例中为微流控芯片）及其控制软件的公司，包括定制芯片设计以满足特定研究人员实验室设备所施加的限制。该项目的影响在于它扩大了微流体技术的可用性，促进了新的微流体应用、新的跨学科研究以及微流体的新商业机会。微流控芯片，该项目旨在开发第一种合成正确构建微流控组件、多组件微流控芯片和微流控程序的技术。该项目研究了一种新颖的反例引导感应微流控合成（CEGIMS）算法。它将微流控芯片合成器和控制程序合成器相结合，以协同地生成微流控芯片设计和可用设备的相应控制软件。用户提供微流控芯片几何形状和控制软件结构的草图，以及指定用户对芯片内部流动的流体物理特性的期望的评估标准，CEGIMS 将物理建模软件与可满足性模理论 (SMT) 集成在一起。求解器依靠反例引导的搜索方法来完成草图，产生适合制造的最终芯片布局，同时，CEGIMS 自动合成控制软件。为了实现这些技术目标，该项目旨在开发技术的根本进步，将基于逻辑正确性属性的求解器与确定物理模型正确性的仿真软件集成。该奖项反映了 NSF 的法定使命。通过使用基金会的智力价值和更广泛的影响审查标准进行评估，并被认为值得支持。

项目成果

Multi-Objective Design Automation for Microfluidic Capture Chips

• DOI: 10.1109/tnb.2022.3212625
• 发表时间: 2022-10
• 期刊: IEEE Transactions on NanoBioscience
• 影响因子: 3.9
• 作者: Lisa Chen;William H. Grover;Manu Sridharan;P. Brisk