SHF: Small: Exascale Formal Verification Algorithms for Parameterized Probabilistic Models of Complex Computational Systems

该项目创建了高性能的算法，用于根据预期行为的形式规范来发现和验证参数化的概率模型。概率模型自然地描述了不确定性对许多真实世界系统行为的影响，包括概率正确的计算设备、自治的网络物理系统和多结果预测模型。计算模型中的参数被用来表示关于所描述的系统的知识的不完备性--要么是由于缺乏足够的实验洞察力，要么是因为需要构建可重复使用的模板设计。这个项目开发的概率系统的分析和综合技术可能会产生广泛的影响，因为许多重要的现实世界系统本质上是概率的。该项目利用贝叶斯风险分析和概率度量变化之间的协同作用来设计新的模型验证算法，以揭示计算模型罕见但有趣的行为。通过利用随机度量嵌入的理论结果和极值计算的实际进展，该项目创建了新的并行算法，用于从一套行为规范合成概率模型的参数。该项目使用生化和网络物理系统的计算模型作为评估的基准，并创建了一个基于网络的网络基础设施，以便将算法迅速传播到更广泛的社区。该项目将加速复杂预测模型的设计，方法是根据多个历史观测数据自动进行验证。它还将启用基于正式方法的不确定性量化框架，用于分析智能网络物理系统的正确性-从而使这些设备更安全。

The project creates high-performance algorithms for discovering and validating parameterized probabilistic models against formal specifications of their expected behavior. Probabilistic models naturally describe the impact of uncertainties on the behavior of many real-world systems including probabilistically correct computing devices, autonomous cyber-physical systems, and multi-outcome predictive models. Parameters in computational models are employed to represent incompleteness in the knowledge about the system being described - either due to a lack of sufficient experimental insight or due to the need for constructing template designs that can be reused. The analysis and synthesis techniques for probabilistic systems developed in this project could have a broad impact since many important real-world systems are probabilistic in nature. The project exploits the synergy between Bayesian risk analysis and change of probability measures to design new model validation algorithms that expose rare but interesting behaviors of computational models. By leveraging theoretical results in randomized metric embeddings and practical advances in extreme-scale computing, the project creates new parallel algorithms for synthesizing parameters of probabilistic models from a suite of behavioral specifications. The project uses computational models of biochemical and cyber-physical systems as benchmarks for evaluation, and creates a web-based cyber-infrastructure for rapid dissemination of the algorithms to the wider community. The project will accelerate the design of complex predictive models by automatically validating them against multiple historical observations. It will also enable a formal methods based uncertainty quantification framework for analyzing the correctness of intelligent cyber-physical systems - thereby, making these devices safer.