{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:26:20Z","timestamp":1748413580960,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030535179"},{"type":"electronic","value":"9783030535186"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53518-6_7","type":"book-chapter","created":{"date-parts":[[2020,7,17]],"date-time":"2020-07-17T15:17:50Z","timestamp":1594999070000},"page":"105-122","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A Framework for Formal Dynamic Dependability Analysis Using HOL Theorem Proving"],"prefix":"10.1007","author":[{"given":"Yassmeen","family":"Elderhalli","sequence":"first","affiliation":[]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,7,17]]},"reference":[{"issue":"1","key":"7_CR1","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1109\/TDSC.2004.2","volume":"1","author":"A Avizienis","year":"2004","unstructured":"Avizienis, A., Laprie, J.C., Randell, B., Landwehr, C.: Basic concepts and taxonomy of dependable and secure computing. IEEE Trans. Dependable Secure Comput. 1(1), 11\u201333 (2004)","journal-title":"IEEE Trans. Dependable Secure Comput."},{"key":"7_CR2","volume-title":"Probability and Statistics with Reliability, Queuing and Computer Science Applications","author":"KS Trivedi","year":"2002","unstructured":"Trivedi, K.S.: Probability and Statistics with Reliability, Queuing and Computer Science Applications. Wiley, Hoboken (2002)"},{"key":"7_CR3","unstructured":"Stamatelatos, M., Vesely, W., Dugan, J., Fragola, J., Minarick, J., Railsback, J.: Fault Tree Handbook with Aerospace Applications. NASA Office of Safety and Mission Assurance (2002)"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Distefano, S., Xing, L.: A new approach to modeling the system reliability: dynamic reliability block diagrams. In: Reliability and Maintainability Symposium, pp. 189\u2013195. IEEE (2006)","DOI":"10.1109\/RAMS.2007.328095"},{"key":"7_CR5","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"7_CR6","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","author":"MJ Gordon","year":"1993","unstructured":"Gordon, M.J., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-66266-4_1","volume-title":"Computer Safety, Reliability, and Security","author":"M Ghadhab","year":"2017","unstructured":"Ghadhab, M., Junges, S., Katoen, J.-P., Kuntz, M., Volk, M.: Model-based safety analysis for vehicle guidance systems. In: Tonetta, S., Schoitsch, E., Bitsch, F. (eds.) SAFECOMP 2017. LNCS, vol. 10488, pp. 3\u201319. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66266-4_1"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/978-3-030-30446-1_27","volume-title":"Software Engineering and Formal Methods","author":"Y Elderhalli","year":"2019","unstructured":"Elderhalli, Y., Volk, M., Hasan, O., Katoen, J.-P., Tahar, S.: Formal verification of rewriting rules for dynamic fault trees. In: \u00d6lveczky, P.C., Sala\u00fcn, G. (eds.) SEFM 2019. LNCS, vol. 11724, pp. 513\u2013531. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30446-1_27"},{"issue":"2","key":"7_CR10","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/j.entcs.2005.10.030","volume":"153","author":"M Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Quantitative analysis with the probabilistic model checker PRISM. Electron. Notes Theor. Comput. Sci. 153(2), 5\u201331 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-319-47677-3_17","volume-title":"Dependable Software Engineering: Theories, Tools, and Applications","author":"W Ahmed","year":"2016","unstructured":"Ahmed, W., Hasan, O.: Formalization of fault trees in higher-order logic: a deep embedding approach. In: Fr\u00e4nzle, M., Kapur, D., Zhan, N. (eds.) SETTA 2016. LNCS, vol. 9984, pp. 264\u2013279. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47677-3_17"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.jal.2016.05.007","volume":"18","author":"W Ahmed","year":"2016","unstructured":"Ahmed, W., Hasan, O., Tahar, S.: Formalization of reliability block diagrams in higher-order logic. J. Appl. Logic 18, 19\u201341 (2016)","journal-title":"J. Appl. Logic"},{"key":"7_CR13","unstructured":"HOL4 (2020). https:\/\/hol-theorem-prover.org\/"},{"key":"7_CR14","first-page":"467","volume":"6","author":"Y Elderhalli","year":"2019","unstructured":"Elderhalli, Y., Ahmad, W., Hasan, O., Tahar, S.: Probabilistic analysis of dynamic fault trees using HOL theorem proving. J. Appl. Logics 6, 467\u2013509 (2019)","journal-title":"J. Appl. Logics"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-030-32409-4_16","volume-title":"Formal Methods and Software Engineering","author":"Y Elderhalli","year":"2019","unstructured":"Elderhalli, Y., Hasan, O., Tahar, S.: A formally verified algebraic approach for dynamic reliability block diagrams. In: Ait-Ameur, Y., Qin, S. (eds.) ICFEM 2019. LNCS, vol. 11852, pp. 253\u2013269. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32409-4_16"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J.: Markov processes in Isabelle\/HOL. In: ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 100\u2013111 (2017)","DOI":"10.1145\/3018610.3018628"},{"key":"7_CR17","unstructured":"Isabelle (2020). https:\/\/isabelle.in.tum.de\/"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-319-20615-8_3","volume-title":"Intelligent Computer Mathematics","author":"W Ahmed","year":"2015","unstructured":"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 (LNAI), vol. 9150, pp. 39\u201354. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8_3"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-642-14052-5_27","volume-title":"Interactive Theorem Proving","author":"T Mhamdi","year":"2010","unstructured":"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\u2013402. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_27"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-22863-6_18","volume-title":"Interactive Theorem Proving","author":"T Mhamdi","year":"2011","unstructured":"Mhamdi, T., Hasan, O., Tahar, S.: Formalization of entropy measures in HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 233\u2013248. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22863-6_18"},{"key":"7_CR21","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.cosrev.2015.03.001","volume":"15\u201316","author":"E Ruijters","year":"2015","unstructured":"Ruijters, E., Stoelinga, M.: Fault tree analysis: a survey of the state-of-the-art in modeling. Anal. Tools Comput. Sci. Rev. 15\u201316, 29\u201362 (2015)","journal-title":"Anal. Tools Comput. Sci. Rev."},{"key":"7_CR22","unstructured":"Merle, G.: Algebraic modelling of dynamic fault trees, contribution to qualitative and quantitative analysis. Ph.D. thesis, ENS, France (2010)"},{"key":"7_CR23","unstructured":"Sullivan, K.J., Dugan, J.B., Coppit, D.: The galileo fault tree analysis tool. In: IEEE Symposium on Fault-Tolerant Computing, pp. 232\u2013235 (1999)"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-319-77935-5_10","volume-title":"NASA Formal Methods","author":"Y Elderhalli","year":"2018","unstructured":"Elderhalli, Y., Hasan, O., Ahmad, W., Tahar, S.: Formal dynamic fault trees analysis using an integration of theorem proving and model checking. In: Dutle, A., Mu\u00f1oz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 139\u2013156. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-77935-5_10"},{"key":"7_CR25","doi-asserted-by":"publisher","first-page":"136176","DOI":"10.1109\/ACCESS.2019.2942829","volume":"7","author":"Y Elderhalli","year":"2019","unstructured":"Elderhalli, Y., Hasan, O., Tahar, S.: A methodology for the formal verification of dynamic fault trees using HOL theorem proving. IEEE Access 7, 136176\u2013136192 (2019)","journal-title":"IEEE Access"},{"key":"7_CR26","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1109\/TDSC.2009.45","volume":"7","author":"H Boudali","year":"2010","unstructured":"Boudali, H., Crouzen, P., Stoelinga, M.: A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Trans. Dependable Secure Comput. 7, 128\u2013143 (2010)","journal-title":"IEEE Trans. Dependable Secure Comput."},{"key":"7_CR27","unstructured":"Altby, A., Majdandzic, D.: Design and implementation of a fault-tolerant drive-by-wire system. Master\u2019s thesis, Chalmers University of Technology, Sweden (2014)"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Distefano, S., Puliafito, A.: Dynamic reliability block diagrams vs dynamic fault trees. In: Reliability and Maintainability Symposium, pp. 71\u201376. IEEE (2007)","DOI":"10.1109\/RAMS.2007.328095"},{"key":"7_CR29","unstructured":"BlockSim (2020). https:\/\/www.reliasoft.com\/products\/reliability-analysis\/blocksim"},{"key":"7_CR30","unstructured":"Distefano, S.: System dependability and performances: techniques, methodologies and tools. Ph.D. thesis, University of Messina, Italy (2005)"},{"key":"7_CR31","unstructured":"Xu, H., Xing, L.: Formal semantics and verification of dynamic reliability block diagrams for system reliability modeling. In: International Conference on Software Engineering and Applications, pp. 155\u2013162 (2007)"},{"key":"7_CR32","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5265-9","volume-title":"The Object-Z Specification Language","author":"G Smith","year":"2012","unstructured":"Smith, G.: The Object-Z Specification Language, vol. 1. Springer, Boston (2012). https:\/\/doi.org\/10.1007\/978-1-4615-5265-9"},{"issue":"2","key":"7_CR33","first-page":"132","volume":"31","author":"H Xu","year":"2009","unstructured":"Xu, H., Xing, L., Robidoux, R.: Drbd: dynamic reliability block diagrams for system reliability modelling. Int. J. Comput. Appl. 31(2), 132\u2013141 (2009)","journal-title":"Int. J. Comput. Appl."},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"Hasan, O., Ahmed, W., Tahar, S., Hamdi, M.S.: Reliability block diagrams based analysis: a survey. In: International Conference of Numerical Analysis and Applied Mathematics, vol. 1648, p. 850129.1-4. AIP (2015)","DOI":"10.1063\/1.4913184"},{"issue":"2","key":"7_CR35","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/s11390-013-1324-6","volume":"28","author":"L Liu","year":"2013","unstructured":"Liu, L., Hasan, O., Tahar, S.: Formal reasoning about finite-state discrete-time Markov chains in HOL. J. Comput. Sci. Technol. 28(2), 217\u2013231 (2013)","journal-title":"J. Comput. Sci. Technol."},{"key":"7_CR36","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198572237.001.0001","volume-title":"Probability and Random Processes","author":"G Grimmett","year":"2001","unstructured":"Grimmett, G., Stirzaker, D., et al.: Probability and Random Processes. Oxford University Press, Oxford (2001)"},{"key":"7_CR37","unstructured":"Elderhalli, Y., Hasan, O., Tahar, S.: Using machine learning to minimize user intervention in theorem proving based dynamic fault tree analysis. In: Conference on Artificial Intelligence and Theorem Proving, pp. 36\u201337 (2019)"},{"key":"7_CR38","doi-asserted-by":"crossref","unstructured":"Li, Y., Lee, P.P.C., Lui, J.C.S.: Stochastic analysis on RAID reliability for solid-state drives. In: IEEE International Symposium on Reliable Distributed Systems, pp. 71\u201380 (2013)","DOI":"10.1109\/SRDS.2013.16"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-53518-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,10]],"date-time":"2024-08-10T07:50:18Z","timestamp":1723276218000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-53518-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030535179","9783030535186"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53518-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bertinoro","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cicm-conference.org\/2020\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}