Formalising and analysing the control software of the Compact Muon Solenoid Experiment at the Large Hadron Collider

被引：13

作者：

Hwong, Yi Ling ^{[1
]}

Keiren, Jeroen J. A. ^{[2
]}

Kusters, Vincent J. J. ^{[1
,3
]}

Leemans, Sander ^{[1
,2
]}

Willemse, Tim A. C. ^{[2
]}

机构：

[1] CERN, European Org Nucl Res, CH-1211 Geneva 23, Switzerland

[2] Eindhoven Univ Technol, Dept Math & Comp Sci, NL-5600 MB Eindhoven, Netherlands

[3] ETH, Inst Theoret Comp Sci, CH-8092 Zurich, Switzerland

来源：

SCIENCE OF COMPUTER PROGRAMMING | 2013年 / 78卷 / 12期

关键词：

Case study; Process algebra; SML; Bounded model checking; Model transformations; OBJECT-ORIENTED FRAMEWORK; MODEL-CHECKING; SYSTEMS; VERIFICATION; SYMMETRY;

D O I：

10.1016/j.scico.2012.11.009

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

The control software of the CERN Compact Muon Solenoid experiment contains over 27 500 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. (C) 2013 Elsevier B.V. All rights reserved.

引用

页码：2435 / 2452

页数：18

共 50 条

[41] Soft error recovery during operation of the compact muon solenoid experiment
Rakness, G.
[J]. JOURNAL OF INSTRUMENTATION, 2013, 8
[42] Susy searches and measurements with the atlas experiment at the large hadron collider
Costanzo, D
[J]. PARTICLES AND THE UNIVERSE, 2004, : 199 - 204
[43] Heavy ion physics with the CMS experiment at the large hadron collider
Wyslouch, B
[J]. JOURNAL OF PHYSICS G-NUCLEAR AND PARTICLE PHYSICS, 2004, 30 (08) : S1149 - S1153
[44] Validation of synthetic diamond for a beam condition monitor for the compact muon solenoid experiment
Chong, D
Fernandez-Hernando, L
Gray, R
Ilgner, CJ
Macpherson, AL
Oh, A
Pritchard, TW
Stone, R
Worm, S
[J]. 2004 IEEE NUCLEAR SCIENCE SYMPOSIUM CONFERENCE RECORD, VOLS 1-7, 2004, : 1812 - 1815
[45] Mechanical and Microstructural Characterisation of Cooling Pipes for the Compact Muon Solenoid Experiment at CERN
Zaburda, George
Onnela, Antti
Cichy, Kamil
Daguin, Jerome
Lunt, Alexander J. G.
[J]. MATERIALS, 2021, 14 (12)
[46] The design of a flexible global calorimeter trigger system for the compact muon solenoid experiment
Brooke, J. J.
Cussans, D. G.
Frazier, R. J. E.
Galagedera, S. B.
Heath, G. P.
Huckvale, B. J.
Nash, S. J.
Newbold, D. M.
Shah, A. A.
[J]. JOURNAL OF INSTRUMENTATION, 2007, 2
[47] The first-level and high-level Muon Triggers of the Compact Muon solenoid experiment at CERN
Sakulin, H
[J]. 2003 IEEE NUCLEAR SCIENCE SYMPOSIUM, CONFERENCE RECORD, VOLS 1-5, 2004, : 288 - 292
[48] Improved control of the betatron coupling in the Large Hadron Collider
Persson, T.
Tomas, R.
[J]. PHYSICAL REVIEW SPECIAL TOPICS-ACCELERATORS AND BEAMS, 2014, 17 (05):
[49] Searches for extra dimensions in the CMS experiment at the Large Hadron Collider (LHC)
Shmatov, S. V.
[J]. PHYSICS OF ATOMIC NUCLEI, 2011, 74 (03) : 490 - 495
[50] Status of the production of GEM chambers for the CMS experiment at Large Hadron Collider
Benussi, L.
Bianco, S.
Campagnola, R.
Caponero, M.
Colafranceschi, S.
Meola, S.
Paoletti, E.
Passamonti, L.
Piccolo, D.
Pierluigi, D.
Russo, A.
Saviano, G.
Tesauro, R.
[J]. NUOVO CIMENTO C-COLLOQUIA AND COMMUNICATIONS IN PHYSICS, 2024, 47 (03):

← 1 2 3 4 5 →