Lifting Formal Proof to Practice via an Assurance Case
Abstract: Formal Methods (FM) are important for verifying properties of systems with mathematical rigor. FM tools and techniques can provide a high level of confidence in a system (software, hardware, etc.), yet a mathematical proof is built on a mathematical model of a system. This gap between the model representation of the system and the operational use of the real-world system is particularly apparent in cyber-physical systems that interact with sensors and actuators, and require reasoning about environmental aspects, such as temperature and wind speed. Assurance cases [2] are a promising approach to bridging this gap, and enabling practical use of FM. We need a way to reason about formal proofs together with assumptions of the operational environment, incorporating evidence on the accuracy of the assumptions. Moreover, a fully verified system is usually an idealistic scenario, and formal proofs are often only available for parts of a system; assurance cases allow one to use FM in context with other forms of evidence, which can speed adoption (e.g., by introducing proofs component-wise).
We present a new form of assurance case evaluation that provides uniform treatment of formal proofand reasoning with evidence, by virtue of a novel Boolean logic over Beta distributions based on efficient, approximate Bayesian inference. The logic enables one to incorporate into one framework a mixture offormally-provable assertions, subjective assertions, and evidence. Further, the logic automatically provides a quantitative estimate of how likely any assertion in the assurance case is expected to hold in practice.
To demonstrate the value of the logic, we present a correct by construction assurance case for a geofence cage ceiling monitor for a drone, inspired by [3]. The monitor for vertical movement runs on an FPGA onboard the Intel Aero platform. The assurance case is a formal proof of monitor soundness and com-pleteness except at the interfaces to the external environment, which are sensors that may not operate asthe monitor software expects. It is at these interfaces that formal proof gives way to evidential reasoningbecause one has only evidence of how sensors behaved after observing them under different physical condi-tions. We show how to incorporate a defeater of the software’s expectations discovered by the STL modelchecker S-Taliro [1] into the assurance case and how it naturally fits into the logic.
Mark Thober is a Principal Professional Staff member at the Johns Hopkins University Applied Physics Laboratory (JHU/APL). He leads the Software Assurance and Formal Methods group at JHU/APL. His interests include automated code analysis, formal methods, programming language-based security, and malware analysis. He is particularly interested in applied research in software assurance, focusing on the impact on real systems and mission needs. He has led research projects for a range of US Government sponsors, including NAVAIR, NAVSEA, DARPA, and FAA. He received his Ph.D. in Computer Science from the Johns Hopkins University.
References
[1] Y. Annapureddy, C. Liu, G. Fainekos, and S. Sankaranarayanan. S-taliro: A tool for temporal logic falsification for hybrid systems.InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS),2011
[2] J. Rushby. The interpretation and evaluation of assurance cases. Technical report, SRI-CSL-15-01, 2015.
[3] J. Stamenkovich, L. Maalolan, and C. Patterson. Formal assurances for autonomous systems without verifying application software.InWorkshop on Research, Education and Development of Unmanned Aerial Systems,pages60–69,2019
-
This work was supported in part by DARPA under agreement number FA8750-20-C-0515. The U.S. Government isauthorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon.Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do notnecessarily reflect those of the sponsor.