Analysing the control software of the Compact Muon Solenoid Experiment at the Large Hadron Collider

Y.L. Hwong, V.J.J. Kusters, T.A.C. Willemse

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review


The control software of the CERN Compact Muon Solenoid experiment contains over 30,000 finite state machines. These state machines are organised hierarchically: commands are sent down the hierarchy and state changes are sent upwards. The sheer size of the system makes it virtually impossible to fully understand the details of its behaviour at the macro level. This is fuelled by unclarities that already exist at the micro level. We have solved the latter problem by formally describing the finite state machines in the mCRL2 process algebra. The translation has been implemented using the ASF+SDF meta-environment, and its correctness was assessed by means of simulations and visualisations of individual finite state machines and through formal verification of subsystems of the control software. Based on the formalised semantics of the finite state machines, we have developed dedicated tooling for checking properties that can be verified on finite state machines in isolation.
Original languageEnglish
Title of host publicationFundamentals of Software Engineering (4th IPM International Conference, FSEN 2011, Tehran, Iran, April 20-22, 2011. Revised Selected Papers)
EditorsF. Arbab, M. Sirjani
Place of PublicationBerlin
ISBN (Print)978-3-642-29319-1
Publication statusPublished - 2012

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Analysing the control software of the Compact Muon Solenoid Experiment at the Large Hadron Collider'. Together they form a unique fingerprint.

Cite this