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

SHF：小型：复杂计算系统参数化概率模型的百亿亿次形式验证算法

• 批准号: 1422257
• 负责人: Sumit Jha
• 金额: $ 48.76万
• 依托单位: The University of Central Florida Board of Trustees
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-07-01 至 2019-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1422257&HistoricalAwards=false
• 关键词: SHF; Small; Exascale; Formal; Verification

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.

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