Skip to main content
SpringerLink
Log in
Book cover

International Conference on Intelligent Computer Mathematics

CICM 2016: Intelligent Computer Mathematics pp 132–147Cite as

Formal Dependability Modeling and Analysis: A Survey

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 9791))

Abstract

Dependability is an umbrella concept that subsumes many key properties about a system, including reliability, maintainability, safety, availability, confidentiality, and integrity. Various dependability modeling techniques have been developed to effectively capture the failure characteristics of systems over time. Traditionally, dependability models are analyzed using paper-and-pencil proof methods and computer based simulation tools but their results cannot be trusted due to their inherent inaccuracy limitations. The recent developments in probabilistic analysis support using formal methods have enabled the possibility of accurate and rigorous dependability analysis. Thus, the usage of formal methods for dependability analysis is widely advocated for safety-critical domains, such as transportation, aerospace and health. Given the complementary strengths of mainstream formal methods, like theorem proving and model checking, and the variety of dependability models judging the most suitable formal technique for a given dependability model is not a straightforward task. In this paper, we present a comprehensive review of existing formal dependability analysis techniques along with their pros and cons for handling a particular dependability model.

The original version of this chapter was revised. The spelling of the author Waqar Ahmad has been corrected. The erratum to this chapter is available at DOI: 10.1007/978-3-319-42547-4_13

An erratum to this chapter can be found at http://dx.doi.org/10.1007/978-3-319-42547-4_13

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   34.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   44.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Avizienis, A., Laprie, J.C., Randell, B.: Fundamental concepts of dependability. Technical report CS-TR-739, Newcastle University, UK (2001). http://pld.ttu.ee/IAF0530/16/avi1.pdf

  2. Spitzer, C.R., Spitzer, C.: Digital Avionics Handbook. CRC Press, Boca Raton (2000)

    Google Scholar 

  3. Al-Kuwaiti, M., Kyriakopoulos, N., Hussein, S.: A comparative analysis of network dependability, fault-tolerance, reliability, security, and survivability. Commun. Surv. Tutorials 11(2), 106–124 (2009)

    Article  Google Scholar 

  4. Weibull: (2015). http://www.weibull.com/hotwire/issue26/relbasics26.htm

  5. Čepin, M.: Reliability block diagram. In: Čepin, M. (ed.) Assessment of Power System Reliability, pp. 119–123. Springer, Heidelberg (2011)

    Google Scholar 

  6. Vesely, W.E., Goldberg, F.F., Roberts, N.H., Haasl, D.F.: Fault tree handbook (NUREG-0492). Technical report, U.S. Nuclear Regulatory Commission (1981)

    Google Scholar 

  7. Gilks, W.R.: Markov Chain Monte Carlo. Wiley, New York (2005)

    Book  Google Scholar 

  8. Trivedi, K.S., Malhotra, M.: Reliability and performability techniques and tools: a survey. In: Walke, B., Spaniol, O. (eds.) Messung, Modellierung und Bewertung von Rechen-und Kommunikationssystemen, pp. 27–48. Springer, New York (1993)

    Chapter  Google Scholar 

  9. Bernardi, S., Merseguer, J., Petriu, D.C.: Dependability modeling and analysis of software systems specified with UML. ACM Comput. Surv. 45(1), 1–48 (2012)

    Article  MATH  Google Scholar 

  10. Venkatesan, L., Shanmugavel, S., Subramaniam, C., et al.: A survey on modeling and enhancing reliability of wireless sensor network. Wirel. Sens. Netw. 5(03), 41–51 (2013)

    Article  Google Scholar 

  11. Trivedi, K.S.: Probability & Statistics with Reliability, Queuing and Computer Science Applications. Wiley, Hoboken (2008)

    MATH  Google Scholar 

  12. Fugua, N.: The applicability of markov analysis methods to reliability, maintainability, and safety. Reliab. Anal. Cent. START Sheet 10(2), 1–8 (2003)

    Google Scholar 

  13. Distefano, S., Xing, L.: A new approach to modeling the system reliability: dynamic reliability block diagrams. In: Reliability and Maintainability Symposium, pp. 189–195. IEEE (2006)

    Google Scholar 

  14. Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice Hall, Upper Saddle River (1981)

    MATH  Google Scholar 

  15. Zhong, D., Qi, Z.: A petri net based approach for reliability prediction of web services. In: Meersman, R., Tari, Z., Herrero, P. (eds.) OTM 2006 Workshops. LNCS, vol. 4277, pp. 116–125. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  16. Yang, X., Li, J., Liu, W., Guo, P.: Petri net model and reliability evaluation for wind turbine hydraulic variable pitch systems. Energies 4(6), 978–997 (2011)

    Article  Google Scholar 

  17. Kumar, G., Jain, V., Gandhi, O.: Reliability and availability analysis of mechanical systems using stochastic petri net modeling based on decomposition approach. Int. J. Reliab. Qual. Safety Eng. 19(01), 1–39 (2012)

    Article  Google Scholar 

  18. Jian, S., Shaoping, W., Yaoxing, S.: Petri-nets based availability model of fault-tolerant server system. In: Robotics, Automation and Mechatronics, pp. 444–449. IEEE (2008)

    Google Scholar 

  19. Dugan, J.B., Ciardo, G.: Stochastic petri net analysis of a replicated file system. Softw. Eng. 15(4), 394–401 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  20. Zengkai, L., Yonghong, L., Ju, L.: Availability and reliability analysis of subsea annular blowout preventer. In: International Conference on Energy, vol. 25, pp. 73–76. Science & Engineering Research Support Society (2013)

    Google Scholar 

  21. Beirong, Z., Xiaowen, X., Wei, X.: Availability modeling and analysis of equipment based on generalized stochastic petri nets. Res. J. Appl. Sci. Eng. Technol. 4(21), 4362–4366 (2012)

    Google Scholar 

  22. Heiner, M., Herajy, M., Liu, F., Rohr, C., Schwarick, M.: Snoopy – a unifying petri net tool. In: Haddad, S., Pomello, L. (eds.) PETRI NETS 2012. LNCS, vol. 7347, pp. 398–407. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  23. Beaudouin-Lafon, M., et al.: CPN/Tools: a tool for editing and simulating coloured petri nets ETAPS tool demonstration related to TACAS. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 574–577. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  24. Wei, B., Lin, C., Kong, X.: Dependability Modeling and Analysis for the Virtual Data Center of Cloud Computing. In: High Performance Computing and Communications, pp. 784–789. IEEE (2011)

    Google Scholar 

  25. Guimarães, A., Maciel, P., Matos Jr., R., Camboim, K.: Dependability analysis in redundant communication networks using reliability importance. In: Information and Network Technology, vol. 4, pp. 12–17. IACSIT Press (2011)

    Google Scholar 

  26. Omidi, A., Moradi, S.: Modeling and quantitative evaluation of an internet voting system based on dependable web services. In: Computer and Communication Engineering, pp. 825–829. IEEE (2012)

    Google Scholar 

  27. Lijie, C., Tao, T., Xianqiong, Z., Schnieder, E.: Verification of the safety communication protocol in train control system using colored Petri net. Reliab. Eng. Syst. Saf. 100, 8–18 (2012)

    Article  Google Scholar 

  28. Li, Y.Z., Yi, H.Y.: Calculation method on reliability of logistics service supply chain based on stochastic petri nets. Int. J. u-and e-Serv. Sci. Technol. 7(1), 103–112 (2014)

    Article  Google Scholar 

  29. Robidoux, R., Xu, H., Xing, L., Zhou, M.: Automated modeling of dynamic reliability block diagrams using colored petri nets. Syst. Man Cybern. Part A Syst. Hum. 40(2), 337–351 (2010)

    Article  Google Scholar 

  30. Nebel, S., Bertsche, B.: Modeling and simulation methodology of the operational availability and logistics using extended colored stochastic petri netsan astronautics case study. In: Reliability and Maintainability Symposium, pp. 434–439. IEEE (2008)

    Google Scholar 

  31. Sadou, N., Demmou, H.: Reliability analysis of discrete event dynamic systems with petri nets. Reliab. Eng. Syst. Saf. 94(11), 1848–1861 (2009)

    Article  Google Scholar 

  32. Balakrishnan, M., Trivedi, K.S.: Stochastic petri nets for the reliability analysis of communication network applications with alternate-routing. Reliab. Eng. Syst. Saf. 52(3), 243–259 (1996)

    Article  Google Scholar 

  33. Radev, D., Rashkova, E., Denchev, V.: Analysis of markov reward models with stochastic petri nets. In: International Conference on Computer Systems and Technologies, pp. 1–6. ACM (2008)

    Google Scholar 

  34. Kohlík, M.: Dependability models based on petri nets and Markov Chains (2009)

    Google Scholar 

  35. Zhu, L., Yu, F.R., Ning, B., Tang, T.: Service availability analysis in communication-based train control systems using WLANs. In: Communications, pp. 1383–1387. IEEE (2012)

    Google Scholar 

  36. Jindal, V., Dharmaraja, S., Trivedi, K.S.: Markov modeling approach for survivability analysis of cellular networks. Int. J. Perform. Eng. 7(5), 429 (2011)

    Google Scholar 

  37. Schoenen, R., Yanikomeroglu, H.: Erlang analysis of cellular networks using stochastic petri nets and user-in-the-loop extension for demand control. In: Global Communication Conference, pp. 298–303. IEEE (2013)

    Google Scholar 

  38. Youness, O., Elkilani, W., El-Wahed, W.A., Torkey, F.: A robust methodology for performance evaluation of communication networks protocols. In: Communication Networks and Services Research Conference, pp. 1–10. IEEE (2006)

    Google Scholar 

  39. Christodoulou, S., Zhou, M.: A petri net approach to modeling and performance analysis of fiber data distributed interface (FDDI) network. In: Emerging Technologies and Factory Automation, pp. 373–380. IEEE (1994)

    Google Scholar 

  40. Ibe, O.C., Choi, H., Trivedi, K.S.: Performance evaluation of client-server systems. Parallel Distrib. Syst. 4(11), 1217–1229 (1993)

    Article  Google Scholar 

  41. Tunik, A., Kharlashkin, I.: A formalistic method for the performance evaluation of communication networks of distributed computing systems. In: Industrial Electronics, vol. 2, pp. 874–878. IEEE (1992)

    Google Scholar 

  42. Sun, X., Lin, C., Liu, W., Xiao, Y.: Survivability evaluation of distributed service using stochastic petri net. In: Communications and Networking in China, pp. 1–5. IEEE (2009)

    Google Scholar 

  43. Zeng, W., Hong, Z.G.: SPN-based performance analysis of LEO satellite networks with multiple users. In: Machine Learning and Cybernetics, vol. 3, pp. 1425–1429. IEEE (2011)

    Google Scholar 

  44. Choi, H., Kulkarni, V.G., Trivedi, K.S.: Markov regenerative stochastic petri nets. Performance Eval. 20(1), 337–357 (1994)

    Article  MathSciNet  Google Scholar 

  45. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  46. Lin, C.M., Yang, C.W., Teng, H.K., Chung, M.C., Lang, K.C., Teng, H.F.: Modeling CAN network using PRISM. In: Industrial Informatics, pp. 390–394. IEEE (2010)

    Google Scholar 

  47. Hermanns, H., Katoen, J.P., Meyer-Kayser, J., Siegle, M.: ETMCC: model checking performability properties of Markov chains. In: Dependable Systems and Networking, p. 1. IEEE (2003)

    Google Scholar 

  48. Pervez, U., Hasan, O., Latif, K., Tahar, S., Gawanmeh, A., Hamdi, M.S.: Formal reliability analysis of a typical FHIR standard based e-Health system using PRISM. In: e-Health Networking, Applications and Services, pp. 43–48. IEEE (2014)

    Google Scholar 

  49. Pervez, U., Mahmood, A., Hasan, O., Latif, K., Gawanmeh, A.: Formal reliability analysis of device interoperability middleware (DIM) based E-health system using PRISM. In: e-Health Networking, Applications and Services, pp. 1–6. IEEE (2015)

    Google Scholar 

  50. Gomes, A., Mota, A., Sampaio, A., Ferri, F., Buzzi, J.: Systematic model-based safety assessment via probabilistic model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part I. LNCS, vol. 6415, pp. 625–639. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  51. Gopinath, K., Elerath, J., Long, D.: Reliability modelling of disk subsystems with probabilistic model checking. Technical report, Technical Report UCSC-SSRC-09-05, University of California, Santa Cruz (2009). http://www.crss.ucsc.edu/media/papers/ssrctr-09-05.pdf

  52. Ge, X., Paige, R.F., McDermid, J.A.: Analysing system failure behaviours with PRISM. In: Secure Software Integration and Reliability Improvement Companion, pp. 130–136. IEEE (2010)

    Google Scholar 

  53. Peng, Z., Lu, Y., Miller, A., Johnson, C., Zhao, T.: A probabilistic model checking approach to analysing reliability, availability, and maintainability of a single satellite system. In: Modelling Symposium, pp. 611–616. IEEE (2013)

    Google Scholar 

  54. Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V.Y., Noll, T., Roveri, M.: The COMPASS approach: correctness, modelling and performability of aerospace systems. In: Buth, B., Rabe, G., Seyfarth, T. (eds.) SAFECOMP 2009. LNCS, vol. 5775, pp. 173–186. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  55. Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  56. Katoen, J.P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: Quantitative Evaluation of Systems, pp. 243–244. IEEE (2005)

    Google Scholar 

  57. Norman, G., Parker, D., Kwiatkowska, M., Shukla, S.: Evaluating the reliability of NAND multiplexing with PRISM. Comput. Aided Des. Integr. Circ. Syst. 24(10), 1629–1637 (2005)

    Article  Google Scholar 

  58. Norman, G., Parker, D.: Quantitative verification: formal guarantees for timeliness. reliability and performance. Technical report (2014)

    Google Scholar 

  59. Conghua, Z., Meiling, C.: Analysis of fast and secure protocol based on continuous-time Markov Chain. Commun. China 10(8), 137–149 (2013)

    Article  Google Scholar 

  60. Hurd, J.: Formal verification of probabilistic algorithms. Ph.D. thesis, University of Cambridge, UK (2002)

    Google Scholar 

  61. Mhamdi, T., Hasan, O., Tahar, S.: On the formalization of the lebesgue integration theory in HOL. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 387–402. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  62. Hölzl, J., Heller, A.: Three chapters of measure theory in Isabelle/HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 135–151. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  63. Hasan, O., Patel, J., Tahar, S.: Formal reliability analysis of combinational circuits using theorem proving. J. Appl. Log. 9(1), 41–60 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  64. Hasan, O., Tahar, S., Abbasi, N.: Formal reliability analysis using theorem proving. Trans. Comput. 59(5), 579–592 (2010)

    Article  MathSciNet  Google Scholar 

  65. Abbasi, N., Hasan, O., Tahar, S.: Formal lifetime reliability analysis using continuous random variables. In: Dawar, A., de Queiroz, R. (eds.) WoLLIC 2010. LNCS, vol. 6188, pp. 84–97. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  66. Ahmed, W., Hasan, O., Tahar, S., Hamdi, M.S.: Towards the formal reliability analysis of oil and gas pipelines. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 30–44. Springer, Heidelberg (2014)

    Google Scholar 

  67. Ahmed, W., Hasan, O., Tahar, S.: Formal reliability analysis of wireless sensor network data transport protocols using HOL. In: Wireless and Mobile Computing, Networking and Communications, pp. 217–224. IEEE (2015)

    Google Scholar 

  68. Ahmed, W., Hasan, O., Tahar, S.: Towards formal reliability analysis of logistics service supply chains using theorem proving. In: Implementation of Logics, pp. 111–121 (2015)

    Google Scholar 

  69. Ahmed, W., Hasan, O.: Towards formal fault tree analysis using theorem proving. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 39–54. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  70. Liu, L., Hasan, O., Tahar, S.: Formal reasoning about finite-state discrete-time markov chains in HOL. J. Comput. Sci. Technol. 28(2), 217–231 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  71. Hölzl, J., Nipkow, T.: Interactive verification of Markov chains: two distributed protocol case studies. arXiv preprint (2012). arXiv:1212.3870

  72. Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28–32. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Acknowledgments

This publication was made possible by NPRP grant # [5 - 813 - 1 - 134] from the Qatar National Research Fund (a member of Qatar Foundation). The statements made herein are solely the responsibility of the author[s].

Author information

Authors and Affiliations

  1. School of Electrical Engineering and Computer Science, National University of Sciences and Technology, Islamabad, Pakistan

    Waqar Ahmad & Osman Hasan

  2. Electrical and Computer Engineering Department, Concordia University, Montreal, Canada

    Sofiène Tahar

Authors
  1. Waqar Ahmad
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Osman Hasan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sofiène Tahar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Waqar Ahmad .

Editor information

Editors and Affiliations

  1. Jacobs University Bremen, Bremen, Germany

    Michael Kohlhase

  2. Chalmers University, Göteborg, Sweden

    Moa Johansson

  3. National Institute of Standards and Technology, Gaithersburg, Maryland, USA

    Bruce Miller

  4. Microsoft Research, Redmond, Washington, USA

    Leonardo de Moura

  5. University of Waterloo, Waterloo, Ontario, Canada

    Frank Tompa

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Ahmad, W., Hasan, O., Tahar, S. (2016). Formal Dependability Modeling and Analysis: A Survey. In: Kohlhase, M., Johansson, M., Miller, B., de Moura, L., Tompa, F. (eds) Intelligent Computer Mathematics. CICM 2016. Lecture Notes in Computer Science(), vol 9791. Springer, Cham. https://doi.org/10.1007/978-3-319-42547-4_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-42547-4_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-42546-7

  • Online ISBN: 978-3-319-42547-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation