Speaker
Description
Ensuring high software reliability is essential for the safe and continuous operation of particle accelerator systems, where failures can have significant operational and safety impacts. Formal methods provide a rigorous approach to improving software reliability by enabling an unambiguous specification, systematic analysis, and exhaustive verification of critical software components, such as programmable logic controller (PLC) programs.
These techniques support multiple reliability-oriented objectives, including formal specification and simulation, automated test case generation, and formal verification. In contrast to traditional testing approaches, formal verification systematically explores the complete state space of program variables, making it particularly effective for identifying rare corner cases that may compromise system reliability.
At CERN, formal methods have been applied to a range of critical software systems, including PLC-based control applications and neural network components used in accelerator environments. This work presents ongoing activities leveraging these methods to improve the reliability of critical software through verification of PLC programs and neural network components, as well as through the formalization of software specifications.