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.

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