Metrics for Assessing the Verifiability of PLC-based Code for Production Automation

Runtime verification is increasingly used to assess the behavior of programmable logic controller software changes against test specifications. In practice, the verification effort varies substantially across different cases. In regulated domains like medical production, evolving technology and compliance requirements frequently introduce changes, the verification becomes attractive for this kind of application to overcome time consuming testing and avoid revalidation eventually. Therefore, this paper proposes a cost model that quantifies verifiability using metrics derived from code-slices (i.e., the code impacted by software changes) and the behavior (timing/repetition of test steps and the number of input combinations) specified in Generalized Test Table (GTT). An evaluation on a baseline code-slice and its variants shows that bit-width-sensitive operand handling and instruction aggregation correlate well with measured verification time, while effects such as operand accessibility and certain interaction patterns are less observable in the experiment. Results on three practical use cases further indicate that the cost of codeslices estimate verification time more consistently than the cost of GTT specification, motivating refined research on how GTT specification contributes to verification cost in the future.