Formal verification of UNICOS-CPC PLC Baseline Objects

During my time at CERN, I worked on the application of formal verification to UNICOS-CPC baseline objects using PLCverif to enhance framework reliability, improve object understanding and minimize extensive testing efforts. The project demonstrated that formal verification can uncover code bugs, difficult to detect through conventional testing. Through analysis of the OnOff object, specific instances of safety requirement violations were identified. Furthermore, clearer specifications were created, including for example the OnOff mode manager and an automated verification pipeline built to streamline testing for new object versions. This project showcases that formal verification not only improves the quality of UNICOS-CPC but also provides a deeper understanding of their behavior, potentially enabling a future model-based development process to build more robust systems and reduce testing workloads.