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 条
  • [1] Large hadron collider physics program: Compact muon solenoid experiment
    J B Singh
    [J]. Pramana, 2000, 54 : 519 - 532
  • [2] Large hadron collider physics program: Compact muon solenoid experiment
    Singh, JB
    [J]. PRAMANA-JOURNAL OF PHYSICS, 2000, 54 (04): : 519 - 532
  • [3] Status of the Compact Muon Solenoid detector at the Large Hadron Collider
    Neal, H
    [J]. B PHYSICS AT HADRON MACHINES, 2004, 722 : 104 - 108
  • [4] Vector Boson scattering from the compact muon solenoid (CMS) experiment at the large hadron collider
    Lu Meng
    Dai ZiLin
    Huang QianMing
    An Ying
    Xiao Jie
    Peng Jing
    Guan Zhe
    Mao YaJun
    Ban Yong
    Li Qiang
    [J]. SCIENTIA SINICA-PHYSICA MECHANICA & ASTRONOMICA, 2021, 51 (08)
  • [5] Separation of signal and background events at the Compact Muon Solenoid of a Large Hadron Collider
    V. B. Gavrilov
    N. V. Il’ina
    O. L. Kodolova
    A. A. Krokhotin
    [J]. Moscow University Physics Bulletin, 2009, 64 : 369 - 373
  • [6] Separation of Signal and Background Events at the Compact Muon Solenoid of a Large Hadron Collider
    Gavrilov, V. B.
    Il'ina, N. V.
    Kodolova, O. L.
    Krokhotin, A. A.
    [J]. MOSCOW UNIVERSITY PHYSICS BULLETIN, 2009, 64 (04) : 369 - 373
  • [7] Tests of the level-1 regional calorimeter trigger for the compact muon solenoid experiment at the large hadron collider
    Chumney, P
    Dasu, S
    Jaworski, M
    Lackey, J
    Robl, P
    Smith, WH
    [J]. 2002 IEEE NUCLEAR SCIENCE SYMPOSIUM, CONFERENCE RECORD, VOLS 1-3, 2003, : 524 - 528
  • [8] Beam-induced radiation in the compact muon solenoid tracker at the Large Hadron Collider
    Singh, A. P.
    Bhat, P. C.
    Mokhov, N. V.
    Beri, S.
    [J]. PRAMANA-JOURNAL OF PHYSICS, 2010, 74 (05): : 719 - 729
  • [9] Higgs search with the Compact Muon Solenoid(CMS) detector at the Large Hadron Collider(LHC)
    Bhattacharya, S
    [J]. INTERNATIONAL JOURNAL OF MODERN PHYSICS A, 2005, 20 (15): : 3400 - 3402
  • [10] Beam-induced radiation in the compact muon solenoid tracker at the Large Hadron Collider
    A. P. Singh
    P. C. Bhat
    N. V. Mokhov
    S. Beri
    [J]. Pramana, 2010, 74 : 719 - 729
12345