Reliability analysis in Symbolic Pathfinder: a brief summary
Antonio Filieri, Corina S. Păsăreanu, Willem I. Visser · Spiral (Imperial College London) · 2014
Designing a software for critical applications requires a precise assessment of reliability.Most of the reliability analysis techniques perform at the architecture level, driving the design since its early stages, but are not directly applicable to source code.We propose a general methodology based on symbolic execution of source code for extracting failure and success paths to be used for probabilistic reliability assessment against relevant usage scenarios.Under the assumption of finite and countable input domains, we provide an efficient implementation based on Symbolic PathFinder that supports the analysis of sequential and parallel Java programs, even with structured data types, at the desired level of confidence.We validated our approach on both NASA prototypes and other test cases showing a promising applicability scope.* This paper reports a summary of (FPV13).Please refer to the original paper for a complete exposition.