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.