Date and Time: Thursday, 08 July 2010, 15:45 - 16:45

Location: HG 6.96

Speaker: Vincent Kusters (MSc student)

Title: Automating the Analysis of the Finite State Machines at CERN

Abstract:

The Large Hadron Collider (LHC), built by the European Organization for Nuclear Research (CERN), is the world's largest particle accelerator. The Compact Muon Solenoid (CMS) is one of the six detectors that have been constructed at the LHC. At a high level, this detector is controlled by a tree of Finite State Machines (FSMs). Every FSM can communicate to its parent and its children in the tree. In order to start the detector, the operator would send the ON command to the root of the tree, after which the appropriate commands propagate down the tree.

The FSM tree for the CMS experiment consists of approximately 20,000 nodes. The sheer size of the tree makes it difficult to understand the behaviour of the system as a whole. To verify the correctness of the system, we have developed tools that can automatically check requirements on an FSM subtree using mCRL2 and Bounded Model Checking (BMC). The tools use the ASF+SDF Meta-Environment to automatically translate FSM source code to mCRL2. In this talk, I will describe these tools and their underlying techniques, give an overview of the problems we encountered and suggest opportunities for further research.