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

点击翻译按钮获取中文摘要

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.