×

Towards the formal reliability analysis of oil and gas pipelines. (English) Zbl 1304.68151

Watt, Stephen M. (ed.) et al., Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-08433-6/pbk). Lecture Notes in Computer Science 8543. Lecture Notes in Artificial Intelligence, 30-44 (2014).
Summary: It is customary to assess the reliability of underground oil and gas pipelines in the presence of excessive loading and corrosion effects to ensure a leak-free transport of hazardous materials. The main idea behind this reliability analysis is to model the given pipeline system as a reliability block diagram (RBD) of segments such that the reliability of an individual pipeline segment can be represented by a random variable. Traditionally, computer simulation is used to perform this reliability analysis but it provides approximate results and requires an enormous amount of CPU time for attaining reasonable estimates. Due to its approximate nature, simulation is not very suitable for analyzing safety-critical systems like oil and gas pipelines, where even minor analysis flaws may result in catastrophic consequences. As an accurate alternative, we propose to use a higher-order-logic theorem prover (HOL) for the reliability analysis of pipelines. As a first step towards this idea, this paper provides a higher-order-logic formalization of reliability and the series RBD using the HOL theorem prover. For illustration, we present the formal analysis of a simple pipeline that can be modeled as a series RBD of segments with exponentially distributed failure times.
For the entire collection see [Zbl 1293.68035].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
90B25 Reliability, availability, maintenance, inspection in operations research

Software:

HOL; ML
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] BP Leak the World’s Worst Accidental Oil Spill, London Telegraph (August 03, 2010), http://www.telegraph.co.uk/finance/newsbysector/energy/oilandgas/7924009/bp-leak-the-worlds-worst-accidental-oil-spill.html (2014)
[2] Zhang, Z., Shao, B.: Reliability Evaluation of Different Pipe Section in Different Period. In: Service Operations and Logistics, and Informatics, pp. 1779–1782. IEEE (2008) · doi:10.1109/SOLI.2008.4682818
[3] Kolowrocki, K.: Reliability and Risk Analysis of Multi-State Systems With Degrading Components. Electronic Journal of International Group on Reliability 2(1), 86–104 (2009)
[4] Soszynska, J.: Reliability and Risk Evaluation of a Port Oil Pipeline Transportation System in Variable Operation conditions. International Journal of Pressure Vessels and Piping 87(2-3), 81–87 (2010) · doi:10.1016/j.ijpvp.2010.01.002
[5] Pipeline Integrity Solution GE-Energy (2014), http://www.ge-energy.com/products_and_services/services/pipeline_integrity_services/
[6] Pipecheck - Pipeline Integrity Assessment Software (2014), http://www.creaform3d.com/en/ndt-solutions/pipecheck-damage-assessment-software
[7] Pandey, D.: Probabilistic Models for Condition Assessment of Oil and Gas Pipelines. Independent Nondestructive Testing and Evaluation International 31(3), 349–358 (1998)
[8] Boca, P., Bowen, J., Siddiqi, J.: Formal Methods: State of the Art and New Directions. Springer (2009) · Zbl 1183.68005
[9] Hasan, O., Tahar, S.: Performance Analysis of ARQ Protocols using a Theorem Prover. In: International Symposium on Performance Analysis of Systems and Software, pp. 85–94. IEEE Computer Society (2008) · doi:10.1109/ISPASS.2008.4510741
[10] Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic Model Checking for Systems Biology. In: Symbolic Systems Biology, pp. 31–59. Jones and Bartlett (2010)
[11] Elleuch, M., Hasan, O., Tahar, S., Abid, M.: Formal Analysis of a Scheduling Algorithm for Wireless Sensor Networks. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 388–403. Springer, Heidelberg (2011) · Zbl 05981982 · doi:10.1007/978-3-642-24559-6_27
[12] Hasan, O., Patel, J., Tahar, S.: Formal Reliability Analysis of Combinational Circuits using Theorem Proving. J. Applied Logic 9(1), 41–60 (2011) · Zbl 1217.94140 · doi:10.1016/j.jal.2011.01.002
[13] Fruth, M.: Formal Methods for the Analysis of Wireless Network Protocols. PhD thesis, Oxford University, UK (2011)
[14] Kaufman, M.: Some Key Research Problems in Automated Theorem Proving for Hardware and Software Verification. Revista de la Real Academia de Ciencias Exactas, Físicas y Naturales. Serie A: Matemáticas 98(1), 181 (2004)
[15] Brown, C.: Automated Reasoning in Higher-order Logic. College Publications (2007) · Zbl 1206.03014
[16] Kapur, D., Subramaniam, M.: Lemma Discovery in Automating Induction. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 538–552. Springer, Heidelberg (1996) · doi:10.1007/3-540-61511-3_112
[17] Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD Thesis, University of Cambridge, UK (2002) · Zbl 1013.68193
[18] 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
[19] 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
[20] Hasan, O., Tahar, S.: Formalization of Continuous Probability Distributions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 3–18. Springer, Heidelberg (2007) · Zbl 1213.68570 · doi:10.1007/978-3-540-73595-3_2
[21] Hasan, O., Tahar, S.: Verification of Tail Distribution Bounds in a Theorem Prover. In: Numerical Analysis and Applied Mathematics, vol. 936, pp. 259–262. American Institute of Physics (2007) · Zbl 1152.60312 · doi:10.1063/1.2790124
[22] Hasan, O., Abbasi, N., Akbarpour, B., Tahar, S., Akbarpour, R.: Formal Reasoning about Expectation Properties for Continuous Random Variables. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 435–450. Springer, Heidelberg (2009) · Zbl 05625550 · doi:10.1007/978-3-642-05089-3_28
[23] Hasan, O., Tahar, S., Abbasi, N.: Formal Reliability Analysis using Theorem Proving. IEEE Transactions on Computers 59(5), 579–592 (2010) · Zbl 1366.94784 · doi:10.1109/TC.2009.165
[24] Abbasi, N., Hasan, O., Tahar, S.: Formal Analysis of Soft Errors using Theorem Proving. In: Symbolic Computation in Software Science. EPTCS, vol. 122, pp. 75–84 (2013) · doi:10.4204/EPTCS.122.7
[25] Abbasi, N., Hasan, O., Tahar, S.: An Approach for Lifetime Reliability Analysis using Theorem Proving. Journal of Computer and System Sciences 80(2), 323–345 (2014) · Zbl 1277.68216 · doi:10.1016/j.jcss.2013.05.002
[26] 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
[27] Bilintion, R., Allan, R.: Reliability Evaluation of Engineering System. Springer (1992) · doi:10.1007/978-1-4899-0685-4
[28] Gordon, M.: Mechanizing Programming Logics in Higher-Order Logic. In: Current Trends in Hardware Verification and Automated Theorem Proving, pp. 387–439. Springer (1989) · doi:10.1007/978-1-4612-3658-0_10
[29] Harrison, J.: Formalized Mathematics. Technical Report 36, Turku Centre for Computer Science (1996)
[30] Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer (1996) · Zbl 0848.68101 · doi:10.1007/978-1-4612-2360-3
[31] Church, A.: A Formulation of the Simple Theory of Types. Journal of Symbolic Logic 5, 56–68 (1940) · Zbl 0023.28901 · doi:10.2307/2266170
[32] Milner, R.: A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences 17, 348–375 (1977) · Zbl 0388.68003 · doi:10.1016/0022-0000(78)90014-4
[33] Ahmad, W.: Formalization of Reliability Block Diagram for Analyzing Oil and Gas Pipelines (2014), http://save.seecs.nust.edu.pk/wahmad/frsaogp.html
[34] Trivedi, K.S.: Probability and Statistics with Reliability, Queuing and Computer Science Applications, 2nd edn. John Wiley and Sons Ltd., Chichester (2002) · Zbl 1344.60003
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.