Developing a Formal Verification Methodology for Safety-Critical Software in Nigerian Oil and Gas Operations

Safety-critical software failures in Nigeria's oil and gas sector have precipitated significant environmental damage, operational losses, and human casualties, yet formal verification practices in the software systems supporting pipeline monitoring, refinery control, and offshore drilling operations remain underdeveloped and un-standardised. This dissertation develops a formal verification methodology for safety-critical software in Nigerian oil and gas operations, contributing an original methodological framework informed by both international standards and the operational realities of Nigeria's South South petroleum industry. A design science research approach is employed across three phases. Phase one conducts a domain analysis of safety-critical software failures at three anonymised Nigerian oil companies in Rivers, Delta, and Bayelsa States through document review and stakeholder interviews with 25 safety engineers and software managers. Phase two develops the Nigerian Oil and Gas Formal Verification Methodology (NOGFVM), integrating model checking using SPIN, theorem proving using Coq, and HAZOP-informed safety requirement formalisation. Phase three applies NOGFVM to three real software components drawn from a consenting operator's pipeline monitoring system, evaluating verification coverage, counterexample discovery rate, and proof construction time. Verification reveals two previously undetected safety-critical race conditions in the pipeline control system components. The dissertation contributes NOGFVM as a publishable methodological artefact, advances formal methods application in African industrial software contexts, and provides recommendations for adoption by the Department of Petroleum Resources. Keywords: formal verification, safety-critical software, oil and gas, Nigeria, model checking