Failure Estimation of Behavioral Specifications

  • Debasmita LoharEmail author
  • Anudeep Dunaboyina
  • Dibyendu Das
  • Soumyajit Dey
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9984)


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.


  1. 1.
    Cheung, R.C.: A user-oriented software reliability model. IEEE Trans. Softw. Eng. 6(2), 118–125 (1980)CrossRefzbMATHGoogle Scholar
  2. 2.
    Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-33826-7_16 CrossRefGoogle Scholar
  3. 3.
    De Loera, J., Dutra, B., Koeppe, M., Moreinis, S., Pinto, G., Wu, J.: Software for exact integration of polynomials over polyhedra. Commun. Comput. Algebra 45(3/4), 169–172 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    De Loera, J.A., Hemmecke, R., Tauzer, J., Yoshida, R.: Effective lattice point counting in rational convex polytopes. J. Symb. Comput. 38(4), 1273–1302 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Denton, J.: Robust, an integrated software reliability tool (1997)Google Scholar
  6. 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
  7. 7.
    Gokhale, S.S.: Architecture-based software reliability analysis: overview and limitations. Trans. Dependable Secur. Comput. 4(1), 32–40 (2007)CrossRefGoogle Scholar
  8. 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
  9. 9.
    Gupta, A., Rybalchenko, A.: InvGen: an efficient invariant generator. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 634–640. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-02658-4_48 CrossRefGoogle Scholar
  10. 10.
    Hsu, C.J., Huang, C.Y.: An adaptive reliability analysis using path testing for complex component-based software systems. Trans. Reliab. 60(1), 158–170 (2011)CrossRefGoogle Scholar
  11. 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
  12. 12.
    Ramani, S., Gokhale, S.S., Trivedi, K.S.: SREPT: software reliability estimation and prediction tool. Perform. Eval. 39(1), 37–60 (2000)CrossRefzbMATHGoogle Scholar
  13. 13.
    Sutherland, J.: Fly-by-wire flight control systems. Technical report, DTIC Document (1968)Google Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  • Debasmita Lohar
    • 1
    Email author
  • Anudeep Dunaboyina
    • 1
  • Dibyendu Das
    • 1
  • Soumyajit Dey
    • 1
  1. 1.Indian Institute of TechnologyKharagpurIndia

Personalised recommendations