A Formal Verification Framework for Mission-Critical Software Systems in Nigerian Oil and Gas Industry Applications

Mission-critical software systems in Nigerian oil and gas industry applications, including SCADA systems, pipeline monitoring, and emergency shutdown controllers, operate in environments where software failures can cause catastrophic human and environmental harm, yet formal verification practices in Nigerian industrial software development are largely absent. This study develops a formal verification framework for mission-critical software systems adapted to Nigerian oil and gas industry contexts. The framework integrates three original contributions: an industrial control system threat model formalised in Event-B notation, capturing the specific hazard scenarios of Nigerian upstream and midstream oil and gas operations, including gas leak detection, well blowout prevention, and sabotage response; a compositional verification methodology that decomposes complex SCADA system specifications into independently verifiable subsystems connected by formal interface contracts, reducing the verification state space to tractable levels; and a certification evidence package format aligned with the IEC 61511 functional safety standard and the Nigerian Oil and Gas Industry Content Development Act 2010, enabling the formal verification outputs to meet Nigerian regulatory certification requirements. The framework was applied to three case study systems provided by a major international oil company operating in Rivers State, achieving formal verification of 78 percent of safety-critical requirements within a four-month project. Residual unverified requirements were triaged and addressed through enhanced testing. The study constitutes an original contribution to formal methods application in African industrial critical infrastructure.

Keywords: formal verification, mission-critical software, oil and gas industry, SCADA, Nigeria