{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T23:38:20Z","timestamp":1767137900133,"version":"build-2238731810"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319478456","type":"print"},{"value":"9783319478463","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47846-3_15","type":"book-chapter","created":{"date-parts":[[2016,10,14]],"date-time":"2016-10-14T02:53:57Z","timestamp":1476413637000},"page":"226-242","source":"Crossref","is-referenced-by-count":2,"title":["Formal Availability Analysis Using Theorem Proving"],"prefix":"10.1007","author":[{"given":"Waqar","family":"Ahmad","sequence":"first","affiliation":[]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,15]]},"reference":[{"key":"15_CR1","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, 2nd edn. Wiley, London (2002)","edition":"2"},{"key":"15_CR2","volume-title":"Handbook of Reliability, Availability, Maintainability and Safety in Engineering Design","author":"RF Stapelberg","year":"2009","unstructured":"Stapelberg, R.F.: Handbook of Reliability, Availability, Maintainability and Safety in Engineering Design. Springer Science & Business Media, Berlin (2009)"},{"issue":"11","key":"15_CR3","doi-asserted-by":"crossref","first-page":"1600","DOI":"10.1109\/12.42134","volume":"38","author":"JT Blake","year":"1989","unstructured":"Blake, J.T., Trivedi, K.S.: Multistage interconnection network reliability. Trans. Comput. 38(11), 1600\u20131604 (1989)","journal-title":"Trans. Comput."},{"key":"15_CR4","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/j.ress.2014.07.012","volume":"132","author":"F Bistouni","year":"2014","unstructured":"Bistouni, F., Jahanshahi, M.: Analyzing the reliability of shuffle-exchange networks using reliability block diagrams. Reliab. Eng. Syst. Saf. 132, 97\u2013106 (2014)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"15_CR5","unstructured":"ReliaSoft (2016). http:\/\/www.reliasoft.com\/"},{"key":"15_CR6","unstructured":"ASENT (2016). https:\/\/www.raytheoneagle.com\/asent\/rbd.htm"},{"issue":"7","key":"15_CR7","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1145\/2639988.2655736","volume":"12","author":"P Bailis","year":"2014","unstructured":"Bailis, P., Kingsbury, K.: The network is reliable. Queue 12(7), 20 (2014)","journal-title":"Queue"},{"issue":"2","key":"15_CR8","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1109\/TSMCA.2009.2034837","volume":"40","author":"R Robidoux","year":"2010","unstructured":"Robidoux, R., Xu, H., Xing, L., Zhou, M.: Automated modeling of dynamic reliability block diagrams using colored Petri nets. IEEE Trans. Syst. Man Cybern. Part A: Syst. Hum. 40(2), 337\u2013351 (2010)","journal-title":"IEEE Trans. Syst. Man Cybern. Part A: Syst. Hum."},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/978-3-642-04468-7_15","volume-title":"Computer Safety, Reliability, and Security","author":"M Bozzano","year":"2009","unstructured":"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\u2013186. Springer, Heidelberg (2009)"},{"key":"15_CR10","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.ress.2012.12.008","volume":"113","author":"JP Signoret","year":"2013","unstructured":"Signoret, J.P., Dutuit, Y., Cacheux, P.J., Folleau, C., Collas, S., Thomas, P.: Make your Petri nets understandable: reliability block diagrams driven Petri nets. Reliab. Eng. Syst. Saf. 113, 61\u201375 (2013)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/978-3-319-08434-3_4","volume-title":"Intelligent Computer Mathematics","author":"W Ahmed","year":"2014","unstructured":"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\u201344. Springer, Heidelberg (2014)"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"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\u2013224. IEEE (2015)","DOI":"10.1109\/WiMOB.2015.7347964"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, vol. 9150, pp. 39\u201354. Springer, Heidelberg (2015)"},{"key":"15_CR15","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","author":"M Gordon","year":"1993","unstructured":"Gordon, M., Melham, T.: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge Press, Cambridge (1993)"},{"key":"15_CR16","unstructured":"Mathematica (2008). www.wolfram.com"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/3-540-57826-9_134","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"J Harrison","year":"1994","unstructured":"Harrison, J., Th\u00e9ry, L.: Extending the HOL theorem prover with a computer algebra system to reason about the reals. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol. 780, pp. 174\u2013184. Springer, Heidelberg (1994)"},{"key":"15_CR18","first-page":"139","volume":"42","author":"HC Wu","year":"2011","unstructured":"Wu, H.C., Wang, C.J., Liu, P.: Reliability analysis of deployment mechanism of solar arrays. Appl. Mech. Mater. 42, 139\u2013142 (2011)","journal-title":"Appl. Mech. Mater."},{"issue":"11","key":"15_CR19","doi-asserted-by":"crossref","first-page":"960","DOI":"10.1016\/j.actaastro.2011.07.012","volume":"69","author":"J Wu","year":"2011","unstructured":"Wu, J., Yan, S., Xie, L.: Reliability analysis method of a solar array by using fault tree analysis and fuzzy reasoning Petri net. Acta Astronaut. 69(11), 960\u2013968 (2011)","journal-title":"Acta Astronaut."},{"key":"15_CR20","volume-title":"An Introduction to Reliability and Maintainability Engineering","author":"CE Ebeling","year":"2004","unstructured":"Ebeling, C.E.: An Introduction to Reliability and Maintainability Engineering. Tata McGraw-Hill Education, Maidenherd (2004)"},{"key":"15_CR21","unstructured":"Ahmed, W.: Formalization of Availability Block Diagram and Unavailability FT (2016). http:\/\/save.seecs.nust.edu.pk\/availability\/"},{"key":"15_CR22","unstructured":"Liu, L.Y.: Formalization of discrete-time Markov chains in HOL. Ph.D. thesis, Concordia University (2013)"}],"updated-by":[{"DOI":"10.1007\/978-3-319-47846-3_30","type":"erratum","label":"Erratum","source":"publisher","updated":{"date-parts":[[2017,3,30]],"date-time":"2017-03-30T00:00:00Z","timestamp":1490832000000}}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47846-3_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,26]],"date-time":"2020-09-26T13:06:35Z","timestamp":1601125595000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47846-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319478456","9783319478463"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47846-3_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}