May 31, 2011: Gijs Kant: Verification of Control Software at CERN

May 31, 2011Verification of Control Software at CERN
Room: Zi 5126Gijs Kant

This talk will be about the purpose and results of a one-week visit to CERN in Geneva, Switzerland. The visit is part of a research project together with TU Eindhoven on verification of the Control Software being developed for the Compact Muon Solenoid (CMS) experiment, part of the Large Hadron Collider (LHC) project. The software is specified as Finite State Machines (FSMs).

In this talk different verification methods will be discussed. Bounded Model Checking in particular has been succesfully applied in the project to find infinite loops. This technique can now easily be used by the developers of the control software.

Another route of verification is by translating modal calculus formulae and process descriptions to Parameterised Boolean Equation Systems (PBESs), but solving them required a lot of time and resources. We apply existing optimisation techniques from Model Checking to solving PBESs to speed up the process and require less memory.
The results of these techniques are still under study. Hopefully they will improve the verification process.