FET: Medium: Collaborative Research: An Efficient Framework for the Stochastic Verification of Computation and Communication Systems Using Emerging Technologies

FET：媒介：协作研究：使用新兴技术对计算和通信系统进行随机验证的有效框架

• 批准号: 1856733
• 负责人: Zhen Zhang
• 金额: $ 39.68万
• 依托单位: Utah State University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-07-15 至 2024-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1856733&HistoricalAwards=false
• 关键词: FET; Medium; Collaborative; Research; Efficient

Synthetic biology and nanotechnology place increasing demands on design methodologies to ensure dependable and robust operation. Consisting of noisy and unreliable components, these complex systems have large and often infinite state spaces that include extremely rare error states. Stochastic model checking techniques have demonstrated significant potential in quantitatively analyzing such system models under extremely low probability. Unfortunately, they generally require enumerating the model's state space, which is computationally intractable or impossible. Therefore, addressing these design challenges in emerging technologies requires enhancing the applicability of stochastic model checking. Motivated by this problem, this project investigates an automated stochastic verification framework that integrates approximate stochastic model checking and counterexample-guided rare-event simulation to improve the analysis accuracy and efficiency. This project focuses on verifying infinite-state continuous-time Markov chain models with rare-event properties. It addresses the scalability problem by first applying property-guided and on-the-fly state truncation techniques to prune unlikely states to obtain finite state representations that are amenable to stochastic model checking. In the case of false or indeterminate verification results, stochastic counterexamples are generated and utilized to improve the accuracy of the state reductions. Furthermore, it mines these critical counterexamples as automated guidance to improve the quality and efficiency for rare-event stochastic simulations. This verification framework will be integrated within existing state-of-the-art stochastic model checking tools, and benchmarked on a wide range of real-world case studies in synthetic biology and nanotechnology.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.

合成生物学和纳米技术对设计方法提出了越来越高的要求，以确保可靠和稳健的操作。这些复杂系统由噪声和不可靠的组件组成，具有大的且通常是无限的状态空间，其中包括极其罕见的错误状态。随机模型检验技术在极低概率下对这类系统模型进行定量分析方面显示出巨大的潜力。不幸的是，它们通常需要枚举模型的状态空间，这在计算上是困难的或不可能的。因此，在新兴技术中解决这些设计挑战需要增强随机模型检验的适用性。受此问题的启发，本课题研究了一种将近似随机模型检验和反例引导的罕见事件模拟相结合的自动化随机验证框架，以提高分析的精度和效率。本项目致力于验证具有稀有事件性质的无限状态连续时间马尔可夫链模型。它首先应用属性引导和动态状态截断技术来修剪不太可能的状态，以获得服从随机模型检查的有限状态表示，从而解决了可伸缩性问题。在验证结果为假或不确定的情况下，生成随机反例，并利用该反例来提高状态约简的精度。此外，它还挖掘这些关键反例作为自动指导，以提高罕见事件随机模拟的质量和效率。这一验证框架将被整合到现有的最先进的随机模型检验工具中，并以合成生物学和纳米技术方面的一系列真实世界案例研究为基准。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Stochastic Hazard Analysis of Genetic Circuits in iBioSim and STAMINA

iBioSim 和 STAMINA 中遗传电路的随机危害分析

• DOI: 10.1021/acssynbio.1c00159
• 发表时间: 2021
• 期刊: ACS synthetic biology
• 影响因子: 4.7
• 作者: Buecherl, Lukas;Roberts, Riley;Fontanarrosa, Pedro;Thomas, Payton J.;Mante, Jeanet;Zhang, Zhen;Myers, Chris J.
• 通讯作者: Myers, Chris J.

A Comparison of Weighted Stochastic Simulation Methods for the Analysis of Genetic Circuits

遗传电路分析的加权随机模拟方法比较

• DOI: 10.1021/acssynbio.2c00553
• 发表时间: 2023
• 期刊: ACS Synthetic Biology
• 影响因子: 4.7
• 作者: Ahmadi, Mohammad;Thomas, Payton J.;Buecherl, Lukas;Winstead, Chris;Myers, Chris J.;Zheng, Hao
• 通讯作者: Zheng, Hao

Efficient Trace Generation for Rare-Event Analysis in Chemical Reaction Networks

化学反应网络中稀有事件分析的高效迹线生成

• 发表时间: 2023
• 期刊: Lecture notes in computer science
• 作者: Israelsen, Bryant;Taylor, Landon;Zhang, Zhen
• 通讯作者: Zhang, Zhen

On Correctness, Precision, and Performance in Quantitative Verification -- QComp 2020 Competition Report

论定量验证的正确性、精确性和性能——QComp 2020竞赛报告

• DOI: 10.1007/978-3-030-83723-5_15
• 发表时间: 2020
• 期刊: Verification and Validation
• 作者: Budde, Carlos E;Hartmanns, Arnd;Klauck, Michaela;Kretinsky, Jan;Parker, David;Quatmann, Tim;Turrini, Andrea;Zhang, Zhen
• 通讯作者: Zhang, Zhen

STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis

• DOI: 10.1007/978-3-030-25540-4_31
• 发表时间: 2019-06
• 期刊: ArXiv
• 作者: Thakur Neupane;C. Myers;C. Madsen;Hao Zheng;Zhen Zhang