Control software of automated production systems evolves to adapt to changing requirements. Quality assurance of such systems after change implementation is to be rigorously obtained for reliable system execution since malfunctions might cause severe issues economi-cally and safety-relatively as socio-technical systems. Considering this target system type and its engineering characteristics, requirements of automation engineers are analyzed regarding control software validation, and a corresponding formal specification approach is pre-sented to be usable by automation engineers. The presented approach targets especially software changes retro-fitting the production automation since software debugging during the commissioning takes quite a large amount of effort required. In addition to the basic notation, its utilization concepts are presented and integrated into the engineering workflow utilizing the expressiveness of the specification in various phases to support control software quality assurance in various ways, from formal verification to run-time monitoring. The approaches are evaluated through application examples, empirical observations, and industry expert feedback to show the approaches’ feasibility, usability, and applicability.weiterlesen