Formal Verification and Compliance Release Control of Cloud-Native Avionics OTA Pipeline Based on GitOps

Abstract

Avionics software is updated more often as OTA practices gain traction, yet current release processes must still meet strict DO-178C requirements. This study introduces a GitOps-based OTA pipeline that links a version-controlled repository with declarative deployment and formal checks. Each merge request triggers TLA+ model checking and automated DO-178C rule matching before rollout. The pipeline was tested in three simulated integration environments and one iron-bird platform, with a total of 420 release runs. The results show a 79.6% reduction in configuration drift, a 54.3% decrease in rollback events, and a rise in early compliance-defect detection to 92.1%. Release-preparation time dropped from 3.4 h to 1.2 h without adding additional reviewers. These findings show that a Git-driven, formally verified pipeline can support safe and repeatable OTA updates and provide a clear audit trail for certification. The approach offers a practical way to connect cloud-native DevOps workflows with avionics assurance needs.