Formal dependability modeling and analysis: a survey. (English) Zbl 1344.68200
Kohlhase, Michael (ed.) et al., Intelligent computer mathematics. 9th international conference, CICM 2016, Bialystok, Poland, July 25–29, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-42546-7/pbk; 978-3-319-42547-4/ebook). Lecture Notes in Computer Science 9791. Lecture Notes in Artificial Intelligence, 132-147 (2016).
Summary: 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.
For the entire collection see [Zbl 1342.68025].
For the entire collection see [Zbl 1342.68025].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
| 68-02 | Research exposition (monographs, survey articles) pertaining to computer science |
Keywords:
reliability block diagrams; fault tree; Markov chain; Petri nets; model checking; higher-order logic; theorem provingReferences:
| [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) |
| [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) · doi:10.1109/SURV.2009.090208 |
| [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) · doi:10.1007/978-0-85729-688-7_9 |
| [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) |
| [7] | Gilks, W.R.: Markov Chain Monte Carlo. Wiley, New York (2005) · doi:10.1002/0470011815.b2a14021 |
| [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) · doi:10.1007/978-3-642-78495-8_3 |
| [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) · Zbl 1293.68075 · doi:10.1145/2379776.2379778 |
| [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) · doi:10.4236/wsn.2013.53006 |
| [11] | Trivedi, K.S.: Probability & Statistics with Reliability, Queuing and Computer Science Applications. Wiley, Hoboken (2008) · Zbl 1344.60003 |
| [12] | Fugua, N.: The applicability of markov analysis methods to reliability, maintainability, and safety. Reliab. Anal. Cent. START Sheet 10(2), 1–8 (2003) |
| [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) · doi:10.1109/RAMS.2006.1677373 |
| [14] | Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice Hall, Upper Saddle River (1981) · Zbl 0461.68059 |
| [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) · doi:10.1007/11915034_34 |
| [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) · doi:10.3390/en4060978 |
| [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) · doi:10.1142/S0218539312500052 |
| [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) · doi:10.1109/RAMECH.2008.4681434 |
| [19] | Dugan, J.B., Ciardo, G.: Stochastic petri net analysis of a replicated file system. Softw. Eng. 15(4), 394–401 (1989) · Zbl 0679.68117 · doi:10.1109/32.16600 |
| [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) |
| [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) |
| [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) · doi:10.1007/978-3-642-31131-4_22 |
| [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) · Zbl 0978.68758 · doi:10.1007/3-540-45319-9_39 |
| [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) · doi:10.1109/HPCC.2011.111 |
| [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) |
| [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) · doi:10.1109/ICCCE.2012.6271332 |
| [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) · doi:10.1016/j.ress.2011.12.010 |
| [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) · doi:10.14257/ijunesst.2014.7.1.10 |
| [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) · doi:10.1109/TSMCA.2009.2034837 |
| [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) |
| [31] | Sadou, N., Demmou, H.: Reliability analysis of discrete event dynamic systems with petri nets. Reliab. Eng. Syst. Saf. 94(11), 1848–1861 (2009) · doi:10.1016/j.ress.2009.06.006 |
| [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) · doi:10.1016/0951-8320(95)00132-8 |
| [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) |
| [34] | Kohlík, M.: Dependability models based on petri nets and Markov Chains (2009) |
| [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) · doi:10.1109/ICC.2012.6364550 |
| [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) |
| [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) · doi:10.1109/GLOCOMW.2013.6825003 |
| [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) · doi:10.1109/CNSR.2006.11 |
| [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) |
| [40] | Ibe, O.C., Choi, H., Trivedi, K.S.: Performance evaluation of client-server systems. Parallel Distrib. Syst. 4(11), 1217–1229 (1993) · doi:10.1109/71.250101 |
| [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) · doi:10.1109/ISIE.1992.279721 |
| [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) · doi:10.1109/CHINACOM.2009.5339706 |
| [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) · doi:10.1109/ICMLC.2011.6016850 |
| [44] | Choi, H., Kulkarni, V.G., Trivedi, K.S.: Markov regenerative stochastic petri nets. Performance Eval. 20(1), 337–357 (1994) · doi:10.1016/0166-5316(94)90021-3 |
| [45] | Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008) · Zbl 1179.68076 |
| [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) |
| [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) · doi:10.1109/DSN.2003.1209982 |
| [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) · doi:10.1109/HealthCom.2014.7001811 |
| [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) |
| [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) · doi:10.1007/978-3-642-16558-0_50 |
| [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) · doi:10.1109/SSIRI-C.2010.32 |
| [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) · doi:10.1109/EMS.2013.102 |
| [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) · doi:10.1007/978-3-642-04468-7_15 |
| [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) · Zbl 1010.68766 · doi:10.1007/3-540-45657-0_29 |
| [56] | Katoen, J.P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: Quantitative Evaluation of Systems, pp. 243–244. IEEE (2005) · doi:10.1109/QEST.2005.2 |
| [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) · doi:10.1109/TCAD.2005.852033 |
| [58] | Norman, G., Parker, D.: Quantitative verification: formal guarantees for timeliness. reliability and performance. Technical report (2014) |
| [59] | Conghua, Z., Meiling, C.: Analysis of fast and secure protocol based on continuous-time Markov Chain. Commun. China 10(8), 137–149 (2013) · doi:10.1109/CC.2013.6633752 |
| [60] | Hurd, J.: Formal verification of probabilistic algorithms. Ph.D. thesis, University of Cambridge, UK (2002) · Zbl 1013.68193 |
| [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) · Zbl 1291.68362 · doi:10.1007/978-3-642-14052-5_27 |
| [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) · Zbl 1342.68287 · doi:10.1007/978-3-642-22863-6_12 |
| [63] | Hasan, O., Patel, J., Tahar, S.: Formal reliability analysis of combinational circuits using theorem proving. J. Appl. Log. 9(1), 41–60 (2011) · Zbl 1217.94140 · doi:10.1016/j.jal.2011.01.002 |
| [64] | Hasan, O., Tahar, S., Abbasi, N.: Formal reliability analysis using theorem proving. Trans. Comput. 59(5), 579–592 (2010) · Zbl 1366.94784 · doi:10.1109/TC.2009.165 |
| [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) · Zbl 1306.90040 · doi:10.1007/978-3-642-13824-9_8 |
| [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) · Zbl 1304.68151 · doi:10.1007/978-3-319-08434-3_4 |
| [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) · doi:10.1109/WiMOB.2015.7347964 |
| [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) |
| [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) · Zbl 1417.68174 · doi:10.1007/978-3-319-20615-8_3 |
| [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) · Zbl 1280.68124 · doi:10.1007/s11390-013-1324-6 |
| [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) · Zbl 1165.68474 · doi:10.1007/978-3-540-71067-7_6 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
