Leveraging Industrial Automation Boundaries and Regulation for Scope Reduction in Software Validation

Automated Production Systems (aPS) in regulated industries such as pharmaceuticals, MedTech, or food and beverages must comply with the stringent validation and documentation requirements of Good Manufacturing Practice (GMP) regulations within the European Union (EU). These obligations create significant burdens for aPS manufacturers, particularly when changes require revalidation through manual integration and system testing. But these prerequisites also enable opportunities for lower-effort software verification, leveraging GMP documentation and boundaries of the automation domain to prove, e.g., that an implemented software change realizes the change specification without side effects. This paper proposes a methodical workflow for deriving software slices suitable for formal verification, while being aligned with automation engineering practices and GMP requirements. It defines assumptions for slice utility based on system modularity, interface expressiveness, and domain boundaries. The approach is validated through a real-world GMP-regulated change from a German MedTech aPS manufacturer, following GAMP 5 guidelines, demonstrating the utility for GMP-regulated aPS engineering and automatic verification of a sliced program segment.