Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baeten, J.C.M., Basten, T., Reniers, M.A.: Process Algebra: Equational Theories of Communicating Processes. Cambridge Tracts in Theoretical Computer Science, vol. 50. Cambridge University Press (2010)
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Computers 58, 118–149 (2003)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Blom, S., van de Pol, J., Weber, M.: LTSmin: Distributed and Symbolic Reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354–359. Springer, Heidelberg (2010)
Franek, B., Gaspar, C.: SMI++ object-oriented framework for designing and implementing distributed control systems. IEEE Transactions on Nuclear Science 52(4), 891–895 (2005)
Gaspar, C., Franek, B.: SMI++—Object-oriented framework for designing control systems for HEP experiments. Computer Physics Communications 110(1–3), 87–90 (1998)
Groote, J.F., Mathijssen, A.H.J., Reniers, M.A., Usenko, Y.S., van Weerdenburg, M.J.: Analysis of distributed systems with mCRL2. In: Process Algebra for Parallel and Distributed Processing, pp. 99–128. Chapman and Hall (2009)
Groote, J.F., Willemse, T.A.C.: Model-checking processes with data. Science of Computer Programming 56(3), 251–273 (2005)
Holme, O., González-Berges, M., Golonka, P., Schmeling, S.: The JCOP Framework. Technical Report CERN-OPEN-2005-027, CERN, Geneva (September 2005)
Hwong, Y.-L., Kusters, V.J.J., Willemse, T.A.C.: Analysing the control software of the Compact Muon Solenoid experiment at the Large Hadron Collider. arxiv.org/abs/1101.5324 (2011)
Klint, P.: A meta-environment for generating programming environments. ACM Trans. Softw. Eng. Methodol. 2(2), 176–201 (1993)
Paolucci, P., Polese, G.: The detector control systems for the cms resistive plate chamber, CERN-CMS-NOTE-2008-036 (2008) see, http://cdsweb.cern.ch/record/1167905
van den Brand, M.G.J., van Deursen, A., Heering, J., de Jong, H.A., de Jonge, M., Kuipers, T., Klint, P., Moonen, L., Olivier, P.A., Scheerder, J., Vinju, J.J., Visser, E., Visser, J.: The ASF+SDF Meta-Environment: A Component-Based Language Development Environment. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol. 2027, pp. 365–370. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hwong, YL., Kusters, V.J.J., Willemse, T.A.C. (2012). Analysing the Control Software of the Compact Muon Solenoid Experiment at the Large Hadron Collider. In: Arbab, F., Sirjani, M. (eds) Fundamentals of Software Engineering. FSEN 2011. Lecture Notes in Computer Science, vol 7141. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29320-7_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-29320-7_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29319-1
Online ISBN: 978-3-642-29320-7
eBook Packages: Computer ScienceComputer Science (R0)