FMitF: Track II: Advancing Probabilistic Verification Tool Development for Synthetic Biology

The field of synthetic biology integrates fundamental engineering principles to design biological systems at the genetic level. These systems have beneficial applications in precision medicine, biosensors, and microbial production. Innovations from this field benefit society by improving treatments for cancer and infectious diseases, providing better access to life-saving drugs, and enhancing crop yields. A challenge to the design of reliable synthetic biological systems is the noisy environments in which they operate. These environments can cause unexpected behaviors that can be rare and detrimental. To ensure the reliability of these systems, provable quantitative guarantees must be provided. Probabilistic model checking (PMC) can provide these guarantees, but current tools struggle with the unique complexities of synthetic biology. This project aims to advance PMC tailored to the unique verification challenges of synthetic biology designs by improving the scalability, automation, and accuracy of PMC. The project’s novelties are a unified and robust PMC framework, an easy-to-use graphical user interface, and integration with existing genetic design automation tools. The project's impacts are a strengthened connection between PMC and synthetic biology and a user-friendly PMC tool for early-stage synthetic biological design, making PMC more accessible to practitioners for designing real-world synthetic biological systems. This project advances principled software tool development for synthetic biology designs. Specifically, it develops correct-by-construction implementation of major prototype PMC tools developed by the investigator's group using verification-aware programming languages, before integrating them as a unified PMC framework. To promote PMC accessibility to synthetic biologists, this project also develops a robust and easy-to-use graphical user interface for the unified PMC framework. This project then integrates this PMC framework into the genetic bio-design automation tool iBioSim. The resulting software tool will be benchmarked on a wide range of real-world case studies in synthetic biology. 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.