From testing to verification: a comprehensive methodology for industrial controls frameworks

Industrial control frameworks frequently rely on object representations to manage complex devices found in the field. However, traditional testing methods often struggle to comprehensively validate internal state transitions of these objects, particularly as their state spaces expand due to increasing complexity and configurability of the objects. This paper introduces a novel testing suite for one of CERN's Industrial Controls Frameworks (UNICOS-CPC), capable of systematically verifying internal state transitions of objects in industrial applications by modeling their state space as a graph. The framework enables developers to define test cases by specifying start states, end states, and commands, while autonomously navigating between states to place objects in the correct initial states of each test case. The test suite also stands out for its extensibility: it decouples test syntax from PLC platform-specific implementations through object-oriented design and OPC UA communication, making it adaptable to diverse industrial control systems and frameworks outside CERN that follow a similar device representation approach. By focusing on individual state transitions rather than complex command sequences, this work simplifies testing of UNICOS-CPC objects and enhances their robustness, allowing for the validation of complex object configurations and behaviours in a transparent manner. Furthermore, this novel testing framework enables an automated workflow to validate scenarios determined by formal verification methods where UNICOS-CPC objects arrive at invalid and undesirable states.