Failure Estimation of Behavioral Specifications
Behavioral specifications are often employed for modeling complex systems at high levels of abstraction. Failure conditions of such systems can naturally be specified as assertions defined over system variables. In that way, such behavioral descriptions can be transformed to imperative programs with annotated failure assertions. In this paper, we present a scalable source code based framework for computing failure probability of such programs under the fail-stop model by applying formal methods. The imprecision in the estimation process resulting from coverage loss due to time, memory bounds and loop invariant synthesis, is also quantified using an upper bound computation. We further discuss the design and implementation of ProPFA (Probabilistic Path-based Failure Analyzer), an automated tool developed for this purpose.
- 5.Denton, J.: Robust, an integrated software reliability tool (1997)Google Scholar
- 6.Filieri, A., Păsăreanu, C.S., Visser, W.: Reliability analysis in symbolic pathfinder. In: International Conference on Software Engineering. IEEE Press (2013)Google Scholar
- 8.Goswami, D., Müller-Gritschneder, D., Basten, T., Schlichtmann, U., Chakraborty, S.: Fault-tolerant embedded control systems for unreliable hardware. In: International Symposium on Integrated Circuits (ISIC). IEEE (2014)Google Scholar
- 11.Lyu, M.R., Nikora, A.P., Farr, W.H.: A systematic and comprehensive tool for software reliability modeling and measurement. In: The 23rd International Symposium on Fault-Tolerant Computing. IEEE (1993)Google Scholar
- 13.Sutherland, J.: Fly-by-wire flight control systems. Technical report, DTIC Document (1968)Google Scholar