一句话：提出 ChemFlow，从化学反应网络模型中推断不变量，用于测试生成与模型验证。
化学反应网络（CRN）将程序编码为抽象化学反应，可编译为 DNA 执行，是构建智能纳米器件的基础。已有随机 CRN 程序测试框架依赖现有程序规约，但规约常缺失，且转换为测试用例耗时且易错。本文提出 ChemFlow，从现有 CRN 模型中抽取三类不变量，并利用这些不变量进行测试生成或针对程序实现的模型验证。作者将 ChemFlow 应用于 13 个 CRN 程序，涵盖玩具例子到含数百个反应的真实生物模型，发现不变量具有较强故障检测能力，且通常比规约派生测试更少不稳定性；在生物模型中，开发者确认部分不变量揭示了生物上不正确或不完整之处，表明该方法可帮助提升模型质量。
Chemical reaction networks (CRNs) are an emerging distributed computational paradigm where programs are encoded as a set of abstract chemical reactions. CRNs can be compiled into DNA strands which perform the computations in vitro, creating a foundation for intelligent nanodevices. Recent research proposed a software testing framework for stochastic CRN programs in simulation, however, it relies on existing program specifications. In practice, specifications are often lacking and when they do exist, transforming them into test cases is time-intensive and can be error prone. In this work, we propose an inference technique called ChemFlow which extracts 3 types of invariants from an existing CRN model. The extracted invariants can then be used for test generation or model validation against program implementations. We applied ChemFlow to 13 CRN programs ranging from toy examples to real biological models with hundreds of reactions. We find that the invariants provide strong fault detection and often exhibit less flakiness than specification derived tests. In the biological models we showed invariants to developers and they confirmed that some of these point to parts of the model that are biologically incorrect or incomplete suggesting we may be able to use ChemFlow to improve model quality.
@inproceedings{GertenMLCMK22,
title = {Inference and test generation using program invariants in chemical reaction networks},
author = {Michael C. Gerten and Alexis L. Marsh and James I. Lathrop and Myra B. Cohen and Andrew S. Miner and Titus H. Klinge},
booktitle = {ICSE},
year = {2022},
doi = {10.1145/3510003.3510176}
}