{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:17:48Z","timestamp":1774023468042,"version":"3.50.1"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2024,5,15]],"date-time":"2024-05-15T00:00:00Z","timestamp":1715731200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,5,15]],"date-time":"2024-05-15T00:00:00Z","timestamp":1715731200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2024,6]]},"DOI":"10.1007\/s10703-024-00448-z","type":"journal-article","created":{"date-parts":[[2024,5,15]],"date-time":"2024-05-15T15:01:42Z","timestamp":1715785302000},"page":"285-325","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Dynamic dependability analysis of shuffle-exchange networks"],"prefix":"10.1007","volume":"62","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4437-2933","authenticated-orcid":false,"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":[[2024,5,15]]},"reference":[{"issue":"4","key":"448_CR1","first-page":"01","volume":"2","author":"R Aggarwal","year":"2008","unstructured":"Aggarwal R, Kaur L (2008) On reliability analysis of fault-tolerant multistage interconnection networks. Int J Comput Sci Secur 2(4):01\u201308","journal-title":"Int J Comput Sci Secur"},{"key":"448_CR2","doi-asserted-by":"crossref","unstructured":"Ahmed W, Hasan O (2015) Towards formal fault tree analysis using theorem proving. In: Intelligent computer mathematics, LNCS 9150. Springer, pp 39\u201354","DOI":"10.1007\/978-3-319-20615-8_3"},{"issue":"1","key":"448_CR3","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, Randell B, Landwehr C (2004) Basic concepts and taxonomy of dependable and secure computing. IEEE Trans Dependable Secure Comput 1(1):11\u201333","journal-title":"IEEE Trans Dependable Secure Comput"},{"key":"448_CR4","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/j.ress.2014.07.012","volume":"132","author":"F Bistouni","year":"2014","unstructured":"Bistouni F, Jahanshahi M (2014) Analyzing the reliability of shuffle-exchange networks using reliability block diagrams. Reliab Eng Syst Saf 132:97\u2013106","journal-title":"Reliab Eng Syst Saf"},{"issue":"4","key":"448_CR5","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1080\/17445760.2018.1496434","volume":"34","author":"F Bistouni","year":"2019","unstructured":"Bistouni F, Jahanshahi M (2019) Determining the reliability importance of switching elements in the shuffle-exchange networks. Int J Parallel Emergent Distrib Syst 34(4):448\u2013476","journal-title":"Int J Parallel Emergent Distrib Syst"},{"key":"448_CR6","doi-asserted-by":"crossref","unstructured":"Distefano S, Puliafito A (2007) Dynamic reliability block diagrams vs dynamic fault trees. In: reliability and maintainability symposium. IEEE, pp 71\u201376","DOI":"10.1109\/RAMS.2007.328095"},{"key":"448_CR7","doi-asserted-by":"crossref","unstructured":"Distefano S, Xing L (2006) A new approach to modeling the system reliability: dynamic reliability block diagrams. In: Reliability and maintainability symposium. IEEE, pp 189\u2013195","DOI":"10.1109\/RAMS.2007.328095"},{"key":"448_CR8","unstructured":"Elderhalli Y (2019) Shuffle-exchange network formal dependability analysis: HOL4 script. Concordia University, Canada. http:\/\/hvg.ece.concordia.ca\/code\/hol\/SEN\/index.php"},{"key":"448_CR9","unstructured":"Elderhalli Y, Ahmad W, Hasan O, Tahar S (2018) Formal probabilistic analysis of dynamic fault trees in HOL4. Tech. rep., Concordia University, Canada. https:\/\/arxiv.org\/abs\/1807.11576"},{"issue":"3","key":"448_CR10","first-page":"469","volume":"2631","author":"Y Elderhalli","year":"2019","unstructured":"Elderhalli Y, Ahmad W, Hasan O, Tahar S (2019) Probabilistic analysis of dynamic fault trees using HOL theorem proving. J Appl Log 2631(3):469","journal-title":"J Appl Log"},{"key":"448_CR11","doi-asserted-by":"crossref","unstructured":"Elderhalli Y, Hasan O, Tahar S A (2019) Formally verified algebraic approach for dynamic reliability block diagrams. In: Formal engineering methods, LNCS 11852. Springer, pp 253\u2013269","DOI":"10.1007\/978-3-030-32409-4_16"},{"key":"448_CR12","doi-asserted-by":"crossref","unstructured":"Elderhalli Y, Hasan O, Tahar S (2019) A formally verified HOL algebra for dynamic reliability block diagrams. Technical report, Concordia University, Canada. http:\/\/arxiv.org\/abs\/1908.01930","DOI":"10.1007\/978-3-030-32409-4_16"},{"key":"448_CR13","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 (2019) A methodology for the formal verification of dynamic fault trees using HOL theorem proving. IEEE Access 7:136176\u2013136192","journal-title":"IEEE Access"},{"key":"448_CR14","doi-asserted-by":"crossref","unstructured":"Elderhalli Y, Volks M, Hasan O, Katoen J, Tahar S (2019) Formal verification of rewriting rules for dynamic fault trees. In: Software engineering and formal methods, LNCS 11724. Springer, pp 513\u2013531","DOI":"10.1007\/978-3-030-30446-1_27"},{"key":"448_CR15","unstructured":"Gauthier T, Kaliszyk C, Urban J (2017) TacticToe: learning to reason with HOL4 tactics. In: Logic for programming, artificial intelligence and reasoning, vol 46, pp 125\u2013143"},{"issue":"4","key":"448_CR16","doi-asserted-by":"publisher","first-page":"588","DOI":"10.1016\/j.apm.2007.01.003","volume":"32","author":"I Gunawan","year":"2008","unstructured":"Gunawan I (2008) Redundant paths and reliability bounds in gamma networks. Appl Math Model 32(4):588\u2013594","journal-title":"Appl Math Model"},{"issue":"3","key":"448_CR17","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1504\/IJRS.2013.057092","volume":"7","author":"I Gunawan","year":"2013","unstructured":"Gunawan I (2013) Reliability prediction of distributed systems using Monte Carlo method. Int J Reliab Saf 7(3):235\u2013248","journal-title":"Int J Reliab Saf"},{"key":"448_CR18","doi-asserted-by":"crossref","unstructured":"Hasan O, Ahmed W, Tahar S, Hamdi MS (2015) Reliability block diagrams based analysis: a survey. In: International conference of numerical analysis and applied maths, vol 1648, p 850129. AIP","DOI":"10.1063\/1.4913184"},{"key":"448_CR19","volume-title":"Computer architecture: a quantitative approach","author":"J Hennessy","year":"2011","unstructured":"Hennessy J, Patterson D (2011) Computer architecture: a quantitative approach. Elsevier, Amsterdam"},{"key":"448_CR20","unstructured":"Jeng M, Siegel H (1986) A fault-tolerant multistage interconnection network for multiprocessor systems using dynamic redundancy. In: International conference on distributed computing systems. IEEE, pp 70\u201377"},{"key":"448_CR21","doi-asserted-by":"crossref","unstructured":"Kumar V, Reddy S (1988) Fault-tolerant multistage interconnection networks for multiprocessor systems. In: Concurrent computations. Springer, pp 495\u2013523","DOI":"10.1007\/978-1-4684-5511-3_25"},{"key":"448_CR22","unstructured":"MATLAB (2017) 2017a, The MathWorks, Natick"},{"key":"448_CR23","unstructured":"Merle G (2010) Algebraic modelling of dynamic fault trees, contribution to qualitative and quantitative analysis. Ph.D. thesis, ENS, France"},{"key":"448_CR24","unstructured":"Mhamdi T (2012) Information-theoretic analysis using theorem proving. Ph.D. thesis, Concordia University, Montreal, QC, Canada"},{"key":"448_CR25","doi-asserted-by":"crossref","unstructured":"Mhamdi T, Hasan O, Tahar S (2010) On the formalization of the Lebesgue integration theory in HOL. In: Interactive theorem proving, LNCS 6172. Springer, pp 387\u2013402","DOI":"10.1007\/978-3-642-14052-5_27"},{"key":"448_CR26","doi-asserted-by":"crossref","unstructured":"Mhamdi T, Hasan O, Tahar S (2011) Formalization of entropy measures in HOL. In: Interactive theorem proving, LNCS 6898. Springer, pp 233\u2013248","DOI":"10.1007\/978-3-642-22863-6_18"},{"key":"448_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: a proof assistant for higher-order logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow T, Wenzel M, Paulson LC (2002) Isabelle\/HOL: a proof assistant for higher-order logic. Springer, Berlin"},{"issue":"14","key":"448_CR28","first-page":"1729","volume":"119","author":"D Panda","year":"2018","unstructured":"Panda D, Dash R, Mishra A, Mohapatra S (2018) Reliability evaluation and analysis of multistage interconnection networks. Int J Pure Appl Math 119(14):1729\u20131737","journal-title":"Int J Pure Appl Math"},{"key":"448_CR29","doi-asserted-by":"crossref","unstructured":"Qasim M, Hasan O, Elleuch M, Tahar S (2016) Formalization of normal random variables in HOL. In: Intelligent computer mathematics, LNCS 9791. Springer, pp 44\u201359","DOI":"10.1007\/978-3-319-42547-4_4"},{"issue":"3","key":"448_CR30","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1080\/02564602.2015.1102098","volume":"33","author":"S Rajkumar","year":"2016","unstructured":"Rajkumar S, Goyal N (2016) Review of multistage interconnection networks reliability and fault-tolerance. IETE Tech Rev 33(3):223\u2013230","journal-title":"IETE Tech Rev"},{"key":"448_CR31","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 (2015) Fault tree analysis: a survey of the state-of-the-art in modeling, analysis and tools. Comput Sci Rev 15\u201316:29\u201362","journal-title":"Comput Sci Rev"},{"key":"448_CR32","unstructured":"Stamatelatos M, Vesely W, Dugan J, Fragola J, Minarick J, Railsback J (2002) Fault tree handbook with aerospace applications. NASA Office of Safety and Mission Assurance"},{"key":"448_CR33","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.procs.2015.07.533","volume":"59","author":"N Yunus","year":"2015","unstructured":"Yunus N, Othman M (2015) Reliability evaluation for shuffle exchange interconnection network. Procedia Comput Sci 59:162\u2013170","journal-title":"Procedia Comput Sci"},{"key":"448_CR34","doi-asserted-by":"crossref","unstructured":"Yunus N, Othman M, Hanapi Z, Kweh Y (2019) Evaluation of replication method in shuffle-exchange network reliability performance. In: Advances in data and information sciences. Springer, pp 271\u2013281","DOI":"10.1007\/978-981-13-0277-0_22"},{"issue":"6","key":"448_CR35","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1080\/02564602.2015.1130595","volume":"33","author":"N Yunus","year":"2016","unstructured":"Yunus N, Othman M, Hanapi Z, Lun K (2016) Reliability review of interconnection networks. IETE Tech Rev 33(6):596\u2013606","journal-title":"IETE Tech Rev"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00448-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-024-00448-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00448-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,3]],"date-time":"2024-06-03T16:12:09Z","timestamp":1717431129000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-024-00448-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,15]]},"references-count":35,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["448"],"URL":"https:\/\/doi.org\/10.1007\/s10703-024-00448-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,5,15]]},"assertion":[{"value":"19 March 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 February 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 May 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}